max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

chore: avoid match_syntax in error messages

Browse source
This commit is contained in:
Leonardo de Moura 2021-05-02 15:57:09 -07:00
parent b8b8cc79a9
commit 59b1f8c143
1 changed files with 2 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

4
src/Lean/Elab/Quotation.lean
View file

@ -383,7 +383,7 @@ private partial def getHeadInfo (alt : Alt) : TermElabM HeadInfo :=
{ info with onMatch := fun taken => match info.onMatch taken with
| covered f exh => covered (fun alt => f alt >>= adaptRhs (`(let $id := discr; $(·)))) exh
| r => r }
| _ => throwErrorAt pat "match_syntax: unexpected pattern kind {pat}"
| _ => throwErrorAt pat "match (syntax) : unexpected pattern kind {pat}"
-- Bind right-hand side to new `let_delayed` decl in order to prevent code duplication
private def deduplicate (floatedLetDecls : Array Syntax) : Alt → TermElabM (Array Syntax × Alt)
@ -406,7 +406,7 @@ private partial def compileStxMatch (discrs : List Syntax) (alts : List Alt) : T
trace[Elab.match_syntax] "match {discrs} with {alts}"
match discrs, alts with
| [], ([], rhs)::_ => pure rhs -- nothing left to match
| _, [] => throwError "non-exhaustive 'match_syntax'"
| _, [] => throwError "non-exhaustive 'match' (syntax)"
| discr::discrs, alt::alts => do
let info ← getHeadInfo alt
let pat := alt.1.head!