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