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

fix: preserve unused let-decls at Meta.transform

Browse source
This commit is contained in:
Leonardo de Moura 2022-02-09 10:10:34 -08:00
parent 3b67c7db81
commit 8fbe7062fa
1 changed files with 3 additions and 3 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

6
src/Lean/Meta/Transform.lean
View file

@ -79,19 +79,19 @@ partial def transform {m} [Monad m] [MonadLiftT MetaM m] [MonadControlT MetaM m]
| Expr.lam n d b c =>
withLocalDecl n c.binderInfo (← visit (d.instantiateRev fvars)) fun x =>
visitLambda (fvars.push x) b
| e => visitPost (← mkLambdaFVars fvars (← visit (e.instantiateRev fvars)))
| e => visitPost (← mkLambdaFVars (usedLetOnly := false) fvars (← visit (e.instantiateRev fvars)))
let rec visitForall (fvars : Array Expr) (e : Expr) : MonadCacheT ExprStructEq Expr m Expr := do
match e with
| Expr.forallE n d b c =>
withLocalDecl n c.binderInfo (← visit (d.instantiateRev fvars)) fun x =>
visitForall (fvars.push x) b
| e => visitPost (← mkForallFVars fvars (← visit (e.instantiateRev fvars)))
| e => visitPost (← mkForallFVars (usedLetOnly := false) fvars (← visit (e.instantiateRev fvars)))
let rec visitLet (fvars : Array Expr) (e : Expr) : MonadCacheT ExprStructEq Expr m Expr := do
match e with
| Expr.letE n t v b _ =>
withLetDecl n (← visit (t.instantiateRev fvars)) (← visit (v.instantiateRev fvars)) fun x =>
visitLet (fvars.push x) b
| e => visitPost (← mkLetFVars fvars (← visit (e.instantiateRev fvars)))
| e => visitPost (← mkLetFVars (usedLetOnly := false) fvars (← visit (e.instantiateRev fvars)))
let visitApp (e : Expr) : MonadCacheT ExprStructEq Expr m Expr :=
e.withApp fun f args => do
visitPost (mkAppN (← visit f) (← args.mapM visit))