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

chore: fix test

Browse source
This commit is contained in:
Leonardo de Moura 2020-08-13 16:55:03 -07:00
parent 69ee44d68e
commit 94689ca91f
1 changed files with 3 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -726,6 +726,8 @@ set_option trace.Meta.isDefEq.delta false
set_option trace.Meta.isDefEq.assign false
#eval tst41
set_option pp.all false
def tst42 : MetaM Unit := do
print "----- tst42 -----";
t ← mkListLit nat [mkNatLit 1, mkNatLit 2];
@ -736,7 +738,7 @@ print t;
check t;
match t.arrayLit? with
| some (_, xs) => do
check $ pure $ xs.size == 2;
check $ pure $ xs.length == 2;
match (xs.get! 0).natLit?, (xs.get! 1).natLit? with
| some 1, some 2 => pure ()
| _, _ => throwOther "nat lits expected"