From 9e42f7ea30397af08d59549a0655640bc27df9cf Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Sat, 4 Feb 2017 13:53:12 -0800 Subject: [PATCH] test(tests/lean/run): add test for meta recursive definition wo recursive equation --- tests/lean/run/rec_meta_issue.lean | 12 ++++++++++++ 1 file changed, 12 insertions(+) create mode 100644 tests/lean/run/rec_meta_issue.lean diff --git a/tests/lean/run/rec_meta_issue.lean b/tests/lean/run/rec_meta_issue.lean new file mode 100644 index 0000000000..24722d2b59 --- /dev/null +++ b/tests/lean/run/rec_meta_issue.lean @@ -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