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

chore(tests/lean/run/1797): add test for #1797

Browse source
This commit is contained in:
Leonardo de Moura 2017-09-05 14:36:51 -07:00
parent cc9de4af58
commit 3af8ca11bc
1 changed files with 6 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

6
tests/lean/run/1797.lean Normal file
View file

@ -0,0 +1,6 @@
example (n : nat) : true :=
begin
cases h : n with m,
{ guard_hyp h := n = nat.zero, admit },
{ guard_hyp h := n = nat.succ m, admit}
end