From 54d0fc043e0afef89f8776be5aebc848c4a78919 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Sat, 11 Sep 2021 04:49:36 -0700 Subject: [PATCH] feat: preserve `Expr.mdata` at `simp` --- src/Lean/Meta/Tactic/Simp/Main.lean | 10 +++++----- 1 file changed, 5 insertions(+), 5 deletions(-) diff --git a/src/Lean/Meta/Tactic/Simp/Main.lean b/src/Lean/Meta/Tactic/Simp/Main.lean index 0b155daf4c..34b5398b4c 100644 --- a/src/Lean/Meta/Tactic/Simp/Main.lean +++ b/src/Lean/Meta/Tactic/Simp/Main.lean @@ -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