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

chore(tests/lean/run/match2): missing test

Browse source
This commit is contained in:
Leonardo de Moura 2016-08-21 15:48:17 -07:00
parent 2d90c73546
commit 6aa2ab6538
1 changed files with 7 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

7
tests/lean/run/match2.lean Normal file
View file

@ -0,0 +1,7 @@
inductive imf (f : nat → nat) : nat → Type
| mk1 : ∀ (a : nat), imf (f a)
| mk2 : imf (f 0 + 1)
definition inv_2 (f : nat → nat) : ∀ (b : nat), imf f b → {x : nat \ x > b} →nat
| .(f a) (imf.mk1 .f a) x := a
| .(f 0 + 1) (imf.mk2 .f) x := subtype.elt_of x