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

fix: but at elimMVarDepsApp

Browse source
This commit is contained in:
Leonardo de Moura 2020-02-10 20:49:43 -08:00
parent f0e2a3cfa4
commit e732eac899
2 changed files with 23 additions and 4 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
src/Init/Lean/MetavarContext.lean
View file

@ -811,7 +811,7 @@ private partial def elimMVarDepsApp (elimMVarDepsAux : Expr → M Expr) (xs : Ar
let processDefault (newF : Expr) : M Expr := do {
if newF.isLambda then do
args ← args.mapM (visit elimMVarDepsAux);
pure $ newF.betaRev args.reverse
elimMVarDepsAux $ newF.betaRev args.reverse
else if newF == f then do
args ← args.mapM (visit elimMVarDepsAux);
pure $ mkAppN newF args

25
tests/lean/run/meta2.lean
View file

@ -556,13 +556,32 @@ pure ()
#eval tst33
def tst34 : MetaM Unit := do
print "----- tst33 -----";
print "----- tst34 -----";
let type := mkSort levelOne;
withLocalDecl `α type BinderInfo.default $ fun α => do
m ← mkFreshExprMVar α;
t ← approxDefEq $ mkLambda #[α] (mkArrow m m);
m ← mkFreshExprMVar type;
t ← mkLambda #[α] (mkArrow m m);
print t;
pure ()
set_option pp.purify_metavars false
#eval tst34
def tst35 : MetaM Unit := do
print "----- tst35 -----";
let type := mkSort levelOne;
withLocalDecl `α type BinderInfo.default $ fun α => do
m1 ← mkFreshExprMVar type;
m2 ← mkFreshExprMVar (mkArrow nat type);
let v := mkLambda `x BinderInfo.default nat m1;
assignExprMVar m2.mvarId! v;
let w := mkApp m2 zero;
t1 ← mkLambda #[α] (mkArrow w w);
print t1;
m3 ← mkFreshExprMVar type;
t2 ← mkLambda #[α] (mkArrow (mkBVar 0) (mkBVar 1));
print t2;
check $ isDefEq t1 t2;
pure ()
#eval tst35