max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2
lean4-htt/library/init/meta
History
Leonardo de Moura ca5439c698 feat(frontends/lean/tactic_notation): add support for tac ; [tac_1, ..., tac_n] notation in interactive tactic mode 
closes #1634

This commit also changes the semantic of `tactic.focus [tac_1, ..., tac_n]`.
It now fails if the number of goals is not `n`.
Before it would only fail if there were more tactics than goals.

@Armael: See tests/lean/run/handthen.lean for examples of the new notation.
2017-06-02 11:38:04 -07:00
..
lean chore(*): remove pos_num and num from stdlib 2017-05-25 18:24:16 -07:00
smt feat(library/init): heterogeneous andthen type class, and tactic.seq_focus implementation 2017-06-02 10:38:27 -07:00
ac_tactics.lean feat(frontends/lean): 'mutual' and 'meta' are now keywords 2016-09-24 10:44:40 -07:00
async_tactic.lean feat(frontends/lean): add support for t.<id> and t.<idx> when t is a composite term 2017-03-28 17:47:49 -07:00
attribute.lean feat(frontends/lean): swap (t) and ``(t) semantics 2017-05-15 09:41:31 -07:00
backward.lean chore(library/init): definition => def 2016-10-06 16:04:12 -07:00
comp_value_tactics.lean feat(frontends/lean): add support for t.<id> and t.<idx> when t is a composite term 2017-03-28 17:47:49 -07:00
congr_lemma.lean refactor(library/init/meta/congr_lemma): cleanup congr_lemma API 2017-01-31 16:46:13 -08:00
constructor_tactic.lean fix(library/init/meta/constructor_tactic): fixes #1598 2017-05-25 09:57:15 -07:00
contradiction_tactic.lean feat(frontends/lean): swap (t) and ``(t) semantics 2017-05-15 09:41:31 -07:00
converter.lean feat(frontends/lean): add support for t.<id> and t.<idx> when t is a composite term 2017-03-28 17:47:49 -07:00
decl_cmds.lean feat(frontends/lean): add support for t.<id> and t.<idx> when t is a composite term 2017-03-28 17:47:49 -07:00
declaration.lean feat(frontends/lean): add support for t.<id> and t.<idx> when t is a composite term 2017-03-28 17:47:49 -07:00
default.lean feat(library/init/meta/well_founded_tactics): add simple tactic for discharging decreasing proofs 2017-05-23 22:07:46 -07:00
environment.lean feat(library/class): add attribute for tracking symbols occurring in instances of type classes 2017-05-01 18:02:30 -07:00
exceptional.lean feat(frontends/lean): change notation for inaccessible patterns 2017-03-28 16:09:15 -07:00
expr.lean refactor(library/init/meta/expr): pure Lean implementation of reflected 2017-06-01 10:17:51 +02:00
format.lean feat(init/meta): add has_to_format instances and prefer direct has_to_tactic_format implementations 2017-04-11 17:07:28 -07:00
fun_info.lean feat(frontends/lean): add support for t.<id> and t.<idx> when t is a composite term 2017-03-28 17:47:49 -07:00
has_reflect.lean refactor(library/init/meta/has_reflect): get rid of unchecked_cast 2017-06-01 10:59:09 +02:00
injection_tactic.lean feat(init/meta/injection_tactic): injections tactic 2017-05-27 06:15:47 -04:00
interaction_monad.lean fix(frontends/lean/tactic_notation): do not clamp errors to the end of {} blocks 2017-05-23 07:28:34 +02:00
interactive.lean feat(library/init/meta/interactive): allow metavars in the show_goal tactic 2017-06-01 19:46:38 -07:00
level.lean feat(frontends/lean/elaborator): coercion from (decidable) Prop to bool 2017-02-14 18:41:32 -08:00
match_tactic.lean feat(library/init/category): add has_map type class, delete fmap 2017-05-01 10:13:02 -07:00
mk_dec_eq_instance.lean refactor(library): remove all instances of `(...) 2017-05-12 19:13:48 +02:00
mk_has_sizeof_instance.lean refactor(init/meta,tools): rename now tactic to done 2017-05-03 11:18:31 +02:00
mk_inhabited_instance.lean refactor(init/meta,tools): rename now tactic to done 2017-05-03 11:18:31 +02:00
name.lean feat(frontends/lean): add support for t.<id> and t.<idx> when t is a composite term 2017-03-28 17:47:49 -07:00
occurrences.lean feat(frontends/lean/elaborator): coercion from (decidable) Prop to bool 2017-02-14 18:41:32 -08:00
options.lean feat(frontends/lean): no global universes in the frontend 2017-02-08 17:23:04 -08:00
pexpr.lean refactor(init/meta/expr): unify expr and pexpr 2017-05-17 10:38:12 -07:00
rb_map.lean feat(frontends/lean): add support for t.<id> and t.<idx> when t is a composite term 2017-03-28 17:47:49 -07:00
rec_util.lean feat(library/init/meta/rec_util): add mk_constructors_fresh_names 2017-06-01 17:04:21 -07:00
relation_tactics.lean feat(frontends/lean): add support for t.<id> and t.<idx> when t is a composite term 2017-03-28 17:47:49 -07:00
rewrite_tactic.lean refactor(library/init/meta): avoid '_core' idiom using default parameters 2017-02-14 09:46:55 -08:00
set_get_option_tactics.lean chore(library/init): definition => def 2016-10-06 16:04:12 -07:00
simp_tactic.lean fix(library/init/meta/simp_tactic): make sure replace_target does not fail due to reducibility settings 2017-05-23 21:43:37 -07:00
tactic.lean feat(frontends/lean/tactic_notation): add support for tac ; [tac_1, ..., tac_n] notation in interactive tactic mode 2017-06-02 11:38:04 -07:00
task.lean feat(init): add default value proofs to the monadic hierarchy 2017-03-27 13:42:08 -07:00
transfer.lean feat(init/relator): some new base theorems for transfer tactic 2017-05-27 04:16:25 -04:00
vm.lean feat(library): add functor, applicative, and monad laws, and prove them correct for non-meta instances 2017-03-27 13:42:08 -07:00
well_founded_tactics.lean feat(library/equations_compiler/wf_rec): provide recursive equations to rel_tac 2017-05-30 16:55:37 -07:00