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-11-10 09:04:23 -08:00
parent 17b8ac894a
commit c3756b49eb
3 changed files with 13 additions and 13 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

12
tests/lean/mvar1.lean
View file

@ -49,12 +49,12 @@ def t1 := lctx5.mkLambda #[α, x, y] $ mkApp f #[α, mkApp g #[x, y], lctx5.mkLa
#eval t1
def mctx1 : MetavarContext := {}
def mctx2 := mctx1.mkDecl `m1 `m1 lctx3 natE
def mctx3 := mctx2.mkDecl `m2 `m2 lctx4 α
def mctx4 := mctx3.mkDecl `m3 `m3 lctx4 natE
def mctx5 := mctx4.mkDecl `m4 `m4 lctx1 (arrow typeE (arrow natE (arrow α natE)))
def mctx6 := mctx5.mkDecl `m5 `m5 lctx5 typeE
def mctx7 := mctx5.mkDecl `m6 `m6 lctx5 (arrow typeE (arrow natE (arrow α natE)))
def mctx2 := mctx1.addExprMVarDecl `m1 `m1 lctx3 natE
def mctx3 := mctx2.addExprMVarDecl `m2 `m2 lctx4 α
def mctx4 := mctx3.addExprMVarDecl `m3 `m3 lctx4 natE
def mctx5 := mctx4.addExprMVarDecl `m4 `m4 lctx1 (arrow typeE (arrow natE (arrow α natE)))
def mctx6 := mctx5.addExprMVarDecl `m5 `m5 lctx5 typeE
def mctx7 := mctx5.addExprMVarDecl `m6 `m6 lctx5 (arrow typeE (arrow natE (arrow α natE)))
def mctx8 := mctx7.assignDelayed `m4 lctx4 #[α, x, y] m3
def mctx9 := mctx8.assignExpr `m3 (mkApp g #[x, y])
def mctx10 := mctx9.assignExpr `m1 a

6
tests/lean/mvar2.lean
View file

@ -40,9 +40,9 @@ def lctx3 := lctx2.mkLocalDecl `x `x m1
def lctx4 := lctx3.mkLocalDecl `y `y (arrow natE (mkApp m3 #[α, x]))
def mctx1 : MetavarContext := {}
def mctx2 := mctx1.mkDecl `m1 `m1 lctx1 typeE
def mctx3 := mctx2.mkDecl `m2 `m2 lctx3 natE
def mctx4 := mctx3.mkDecl `m3 `m3 lctx1 (arrow typeE (arrow natE natE))
def mctx2 := mctx1.addExprMVarDecl `m1 `m1 lctx1 typeE
def mctx3 := mctx2.addExprMVarDecl `m2 `m2 lctx3 natE
def mctx4 := mctx3.addExprMVarDecl `m3 `m3 lctx1 (arrow typeE (arrow natE natE))
def mctx5 := mctx4.assignDelayed `m3 lctx3 #[α, x] m2
def mctx6 := mctx5.assignExpr `m2 (arrow α α)
def mctx7 := mctx6.assignExpr `m1 natE

8
tests/lean/mvar3.lean
View file

@ -46,10 +46,10 @@ def lctx3 := lctx2.mkLocalDecl `x `x m1
def lctx4 := lctx3.mkLocalDecl `y `y (arrow natE m2)
def mctx1 : MetavarContext := {}
def mctx2 := mctx1.mkDecl `m1 `m1 lctx2 typeE
def mctx3 := mctx2.mkDecl `m2 `m2 lctx3 natE
def mctx4 := mctx3.mkDecl `m3 `m3 lctx3 natE
def mctx4' := mctx3.mkDecl `m3 `m3 lctx3 natE true
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 R1 :=
match mkLambda mctx4 {namePrefix := `n} lctx4 #[α, x, y] $ mkApp f #[m3, x] with