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

fix: discriminant info tree term

Browse source
This commit is contained in:
Sebastian Ullrich 2022-08-07 18:37:17 +02:00 • committed by Leonardo de Moura
parent 757da9f6f3
commit ed754725e6
1 changed files with 1 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
src/Lean/Elab/Match.lean
View file

@ -62,7 +62,7 @@ private def elabAtomicDiscr (discr : Syntax) : TermElabM Expr := do
| some e@(Expr.fvar fvarId) =>
let localDecl ← fvarId.getDecl
if !isAuxDiscrName localDecl.userName then
addTermInfo discr e -- it is not an auxiliary local created by `expandNonAtomicDiscrs?`
addTermInfo term e -- it is not an auxiliary local created by `expandNonAtomicDiscrs?`
else
instantiateMVars localDecl.value
| _ => throwErrorAt discr "unexpected discriminant"