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

test: add getUnify basic tests

Browse source
This commit is contained in:
Leonardo de Moura 2019-11-24 08:41:00 -08:00
parent 6af26ede2b
commit 2cf3e197aa
1 changed files with 15 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

17
tests/lean/run/meta3.lean
View file

@ -39,11 +39,24 @@ do let d : DiscrTree Nat := {};
mvar ← mkFreshExprMVar nat;
d ← d.insert (mkAppN add #[mvar, mkNatLit 10]) 1;
d ← d.insert (mkAppN add #[mkNatLit 0, mkNatLit 10]) 2;
d ← d.insert (mkAppN (mkConst `Nat.add) #[mkNatLit 0, mkNatLit 10]) 3;
d ← d.insert mvar 4;
d ← d.insert (mkAppN (mkConst `Nat.add) #[mkNatLit 0, mkNatLit 20]) 3;
d ← d.insert (mkAppN add #[mvar, mkNatLit 20]) 4;
d ← d.insert mvar 5;
print (format d);
vs ← d.getMatch (mkAppN add #[mkNatLit 1, mkNatLit 10]);
print (format vs);
let t := mkAppN add #[mvar, mvar];
print t;
vs ← d.getMatch t;
print (format vs);
vs ← d.getUnify t;
print (format vs);
vs ← d.getUnify mvar;
print (format vs);
vs ← d.getUnify $ mkAppN add #[mkNatLit 0, mvar];
print (format vs);
vs ← d.getUnify $ mkAppN add #[mvar, mkNatLit 20];
print (format vs);
pure ()
#eval run [`Init.Data.Nat] tst1