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

fix: ignore Expr.MData at deltaRHS?

Browse source
This commit is contained in:
Leonardo de Moura 2021-12-16 16:58:10 -08:00
parent de29657594
commit e38fab1b4e
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/PreDefinition/Structural/Eqns.lean
View file

@ -27,7 +27,7 @@ def deltaLHS (mvarId : MVarId) : MetaM MVarId := withMVarContext mvarId do
def deltaRHS? (mvarId : MVarId) (declName : Name) : MetaM (Option MVarId) := withMVarContext mvarId do
let target ← getMVarType' mvarId
let some (_, lhs, rhs) ← target.eq? | throwTacticEx `deltaRHS mvarId "equality expected"
let some rhs ← delta? rhs (. == declName) | return none
let some rhs ← delta? rhs.consumeMData (. == declName) | return none
replaceTargetDefEq mvarId (← mkEq lhs rhs)
private partial def whnfAux (e : Expr) : MetaM Expr := do