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

feat: preserve Expr.mdata at simp

Browse source
This commit is contained in:
Leonardo de Moura 2021-09-11 04:49:36 -07:00
parent f26c905130
commit 54d0fc043e
1 changed files with 5 additions and 5 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

10
src/Lean/Meta/Tactic/Simp/Main.lean
View file

@ -155,18 +155,18 @@ where
simpStep (e : Expr) : M Result := do
match e with
| Expr.mdata _ e _ => simp e
| Expr.proj .. => pure { expr := (← reduceProj e) }
| Expr.mdata m e _ => let r ← simp e; return { r with expr := mkMData m r.expr }
| Expr.proj .. => return { expr := (← reduceProj e) }
| Expr.app .. => simpApp e
| Expr.lam .. => simpLambda e
| Expr.forallE .. => simpForall e
| Expr.letE .. => simpLet e
| Expr.const .. => simpConst e
| Expr.bvar .. => unreachable!
| Expr.sort .. => pure { expr := e }
| Expr.sort .. => return { expr := e }
| Expr.lit .. => simpLit e
| Expr.mvar .. => pure { expr := (← instantiateMVars e) }
| Expr.fvar .. => pure { expr := (← reduceFVar (← getConfig) e) }
| Expr.mvar .. => return { expr := (← instantiateMVars e) }
| Expr.fvar .. => return { expr := (← reduceFVar (← getConfig) e) }
congrDefault (e : Expr) : M Result :=
withParent e <| e.withApp fun f args => do