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

test(tests/lean/run): add test for meta recursive definition wo recursive equation

Browse source
This commit is contained in:
Leonardo de Moura 2017-02-04 13:53:12 -08:00
parent 523a576bbe
commit 9e42f7ea30
1 changed files with 12 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

12
tests/lean/run/rec_meta_issue.lean Normal file
View file

@ -0,0 +1,12 @@
open tactic
meta def left_right_search (tac := assumption) : tactic unit :=
tac
<|> (left >> left_right_search)
<|> (right >> left_right_search)
example (p q r : Prop) : r → p ∨ q ∨ r :=
begin intros, left_right_search end
example (a b c : nat) : a = b ∨ b = c ∨ a = a :=
begin left_right_search reflexivity end