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

fix: avoid redundant let-decls

Browse source
This commit is contained in:
Leonardo de Moura 2019-11-09 12:30:58 -08:00
parent 1e065d495b
commit adcb9091ef
2 changed files with 12 additions and 6 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

9
library/Init/Lean/LocalContext.lean
View file

@ -250,9 +250,12 @@ xs.size.foldRev (fun i b =>
else
Expr.forallE n bi ty b
| some (LocalDecl.ldecl _ _ n ty val) =>
let ty := ty.abstractRange i xs;
let val := val.abstractRange i xs;
Expr.letE n ty val b
if b.hasLooseBVar 0 then
let ty := ty.abstractRange i xs;
let val := val.abstractRange i xs;
Expr.letE n ty val b
else
b
| none => panic! "unknown free variable") b
def mkLambda (lctx : LocalContext) (xs : Array Expr) (b : Expr) : Expr :=

9
library/Init/Lean/MetavarContext.lean
View file

@ -567,9 +567,12 @@ do e ← abstractRange elimMVarDeps lctx xs xs.size e;
else
pure $ Expr.forallE n bi type e
| some (LocalDecl.ldecl _ _ n type value) => do
type ← abstractRange elimMVarDeps lctx xs i type;
value ← abstractRange elimMVarDeps lctx xs i value;
pure $ Expr.letE n type value e
if e.hasLooseBVar 0 then do
type ← abstractRange elimMVarDeps lctx xs i type;
value ← abstractRange elimMVarDeps lctx xs i value;
pure $ Expr.letE n type value e
else
pure e
| none => panic! "unknown free variable")
e