From bfae8f347b08545d5d19109fb45e0299fbf8f407 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Fri, 18 Nov 2016 12:51:53 -0800 Subject: [PATCH] feat(library/init/meta/interactive): cases tactic takes arbitrary expressions --- library/init/meta/interactive.lean | 8 +++++++- 1 file changed, 7 insertions(+), 1 deletion(-) diff --git a/library/init/meta/interactive.lean b/library/init/meta/interactive.lean index e938409ba5..b5d21a5fbb 100644 --- a/library/init/meta/interactive.lean +++ b/library/init/meta/interactive.lean @@ -198,7 +198,13 @@ do e ← to_expr p, meta def cases (p : qexpr0) (ids : with_ident_list) : tactic unit := do e ← to_expr p, - cases_core semireducible e ids + if e^.is_local_constant then + cases_core semireducible e ids + else do + x ← mk_fresh_name, + tactic.generalize e x <|> fail "cases tactic failed to generalize given expression", + h ← tactic.intro1, + cases_core semireducible h ids meta def generalize (p : qexpr) (x : ident) : tactic unit := do e ← to_expr p,