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

test: equational theorem test

Browse source
This commit is contained in:
Leonardo de Moura 2021-09-19 09:34:08 -07:00
parent 82f3042fa4
commit fe55205105
1 changed files with 11 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

11
tests/lean/run/structuralEqns2.lean
View file

@ -15,3 +15,14 @@ def g (i j : Nat) : Nat :=
#check g.eq_1
#check g.eq_2
#check g.eq_3
def h (i j : Nat) : Nat :=
let z :=
match j with
| Nat.zero => 1
| Nat.succ j => h i j
z + z
#eval tst ``h
#check h.eq_1
#check h.eq_2