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

chore: fix tests

Browse source
This commit is contained in:
Leonardo de Moura 2019-12-17 07:37:58 -08:00
parent 1b9fb2f726
commit 65edd6e37c
2 changed files with 2 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
tests/lean/mvar3.lean
View file

@ -49,7 +49,7 @@ def mctx1 : MetavarContext := {}
def mctx2 := mctx1.addExprMVarDecl `m1 `m1 lctx2 #[] typeE
def mctx3 := mctx2.addExprMVarDecl `m2 `m2 lctx3 #[] natE
def mctx4 := mctx3.addExprMVarDecl `m3 `m3 lctx3 #[] natE
def mctx4' := mctx3.addExprMVarDecl `m3 `m3 lctx3 #[] natE true
def mctx4' := mctx3.addExprMVarDecl `m3 `m3 lctx3 #[] natE MetavarKind.syntheticOpaque
def R1 :=
match mkLambdaTest mctx4 {namePrefix := `n} lctx4 #[α, x, y] $ mkAppN f #[m3, x] with

2
tests/lean/run/tactic.lean
View file

@ -11,7 +11,7 @@ set_option trace.Meta.Tactic true
def tst1 : MetaM Unit :=
do cinfo ← getConstInfo `simple;
mvar ← mkFreshExprSyntheticMVar cinfo.type;
mvar ← mkFreshExprSyntheticOpaqueMVar cinfo.type;
let mvarId := mvar.mvarId!;
(_, mvarId) ← introN mvarId 4;
assumption mvarId;