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

feat(init/meta/interactive): add generalizing parameter to induction

Browse source
This commit is contained in:
Sebastian Ullrich 2017-04-11 13:33:07 +02:00 • committed by Leonardo de Moura
parent 17204f9629
commit 8ea2bc08cb
3 changed files with 11 additions and 5 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -336,8 +336,13 @@ do e_type ← infer_type e >>= whnf,
(const I ls) ← return $ get_app_fn e_type,
return I
meta def induction (p : parse texpr) (rec_name : parse using_ident) (ids : parse with_ident_list) : tactic unit :=
do e ← i_to_expr p, tactic.induction e ids rec_name, return ()
meta def induction (p : parse texpr) (rec_name : parse using_ident) (ids : parse with_ident_list)
(revert : parse $ (tk "generalizing" *> ident*)?) : tactic unit :=
do e ← i_to_expr p,
locals ← get_locals $ revert.get_or_else [],
n ← revert_lst locals,
tactic.induction e ids rec_name,
all_goals (intron n)
meta def cases (p : parse texpr) (ids : parse with_ident_list) : tactic unit :=
do e ← i_to_expr p,

5
library/init/meta/smt/interactive.lean
View file

@ -219,8 +219,9 @@ smt_tactic.repeat t
meta def all_goals (t : itactic) : smt_tactic unit :=
smt_tactic.all_goals t
meta def induction (p : parse texpr) (rec_name : parse using_ident) (ids : parse with_ident_list) : smt_tactic unit :=
slift (tactic.interactive.induction p rec_name ids)
meta def induction (p : parse texpr) (rec_name : parse using_ident) (ids : parse with_ident_list)
(revert : parse $ (tk "generalizing" *> ident*)?) : smt_tactic unit :=
slift (tactic.interactive.induction p rec_name ids revert)
open tactic

2
src/frontends/lean/token_table.cpp
View file

@ -96,7 +96,7 @@ void init_token_table(token_table & t) {
{"@@", g_max_prec}, {"@", g_max_prec},
{"sorry", g_max_prec}, {"+", g_plus_prec}, {"->", g_arrow_prec}, {"<-", 0},
{"match", 0}, {"^.", g_max_prec+1},
{"renaming", 0}, {"extends", 0}, {nullptr, 0}};
{"renaming", 0}, {"extends", 0}, {"generalizing", 0}, {nullptr, 0}};
char const * commands[] =
{"theorem", "axiom", "axioms", "variable", "protected", "private",