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

feat(library/init/meta/interactive): cases tactic takes arbitrary expressions

Browse source
This commit is contained in:
Leonardo de Moura 2016-11-18 12:51:53 -08:00
parent 866eaae8ed
commit bfae8f347b
1 changed files with 7 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

8
library/init/meta/interactive.lean
View file

@ -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,