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

chore: use headBeta on type

Browse source
This commit is contained in:
Leonardo de Moura 2020-07-24 15:34:19 -07:00
parent 7f43d01703
commit 9dc5ca66e2
1 changed files with 2 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
src/Lean/MetavarContext.lean
View file

@ -769,9 +769,11 @@ xs.size.foldRevM
let x := xs.get! i;
match lctx.getFVar! x with
| LocalDecl.cdecl _ _ n type bi => do
let type := type.headBeta;
type ← abstractRangeAux elimMVarDeps xs i type;
pure $ Lean.mkForall n bi type e
| LocalDecl.ldecl _ _ n type value => do
let type := type.headBeta;
type ← abstractRangeAux elimMVarDeps xs i type;
value ← abstractRangeAux elimMVarDeps xs i value;
let e := mkLet n type value e;