| .. |
|
backward
|
|
|
|
smt
|
refactor(library): mk_result/get_result_* ~> mk_success/get_success_*
|
2018-03-01 14:56:01 +01:00 |
|
ac_tactics.cpp
|
feat(library): add implementation of abstract_context_cache
|
2018-02-21 15:04:20 -08:00 |
|
ac_tactics.h
|
chore(library/tactic): ac_manager ==> ac_manager_old
|
2018-02-01 12:39:43 -08:00 |
|
algebraic_normalizer.cpp
|
chore(*): typos
|
2017-06-07 10:09:38 -07:00 |
|
algebraic_normalizer.h
|
feat(library): add implementation of abstract_context_cache
|
2018-02-21 15:04:20 -08:00 |
|
app_builder_tactics.cpp
|
|
|
|
app_builder_tactics.h
|
|
|
|
apply_tactic.cpp
|
feat(library/tactic): use new cache in the apply and simp tactics
|
2018-02-21 15:04:20 -08:00 |
|
apply_tactic.h
|
feat(library/init/meta): add unify config option to apply_cfg
|
2018-01-04 12:51:59 -08:00 |
|
assert_tactic.cpp
|
chore(library): use type_context to update metavar_context
|
2018-02-27 12:23:26 -08:00 |
|
assert_tactic.h
|
|
|
|
cases_tactic.cpp
|
chore(library): use type_context to update metavar_context
|
2018-02-27 12:23:26 -08:00 |
|
cases_tactic.h
|
|
|
|
change_tactic.cpp
|
chore(library/tactic/change_tactic): use type_context instead of metavar_context
|
2018-02-27 10:41:11 -08:00 |
|
change_tactic.h
|
|
|
|
clear_tactic.cpp
|
fix(msvc): further work on MSVC port
|
2018-02-06 10:11:10 -08:00 |
|
clear_tactic.h
|
|
|
|
CMakeLists.txt
|
feat(library/tactic): add hole_command bookkeeping
|
2017-06-13 21:12:29 -07:00 |
|
congr_lemma_tactics.cpp
|
refactor(library/congr_lemma): remove mk_rel_iff_congr_lemma and mk_rel_eq_congr_lemma
|
2018-02-21 15:04:20 -08:00 |
|
congr_lemma_tactics.h
|
|
|
|
destruct_tactic.cpp
|
fix(library/tactic/destruct_tactic): fixes #1766
|
2017-08-02 15:35:33 +01:00 |
|
destruct_tactic.h
|
|
|
|
dsimplify.cpp
|
refactor(library): mk_result/get_result_* ~> mk_success/get_success_*
|
2018-03-01 14:56:01 +01:00 |
|
dsimplify.h
|
feat(library): add implementation of abstract_context_cache
|
2018-02-21 15:04:20 -08:00 |
|
elaborate.cpp
|
feat(library/init/meta/tactic): add option for not creating new subgoals at to_expr
|
2017-06-28 16:46:29 -07:00 |
|
elaborate.h
|
|
|
|
elaborator_exception.cpp
|
|
|
|
elaborator_exception.h
|
|
|
|
eqn_lemmas.cpp
|
feat(library/tactic/eqn_lemmas): store flag indicating whether a declaration has only simple equation lemmas or not
|
2018-01-16 16:55:05 -08:00 |
|
eqn_lemmas.h
|
feat(library/tactic/eqn_lemmas): store flag indicating whether a declaration has only simple equation lemmas or not
|
2018-01-16 16:55:05 -08:00 |
|
eval.cpp
|
feat(library/tactic, frontends/lean): replace a few mk_tagged_fresh_name with mk_unused_name
|
2018-02-21 15:04:19 -08:00 |
|
eval.h
|
|
|
|
exact_tactic.cpp
|
feat(library/tactic): use new cache
|
2018-02-21 15:04:20 -08:00 |
|
exact_tactic.h
|
|
|
|
fun_info_tactics.cpp
|
|
|
|
fun_info_tactics.h
|
|
|
|
generalize_tactic.cpp
|
chore(library): use type_context to update metavar_context
|
2018-02-27 12:23:26 -08:00 |
|
generalize_tactic.h
|
|
|
|
gexpr.cpp
|
|
|
|
gexpr.h
|
|
|
|
hole_command.cpp
|
feat(shell/server,frontends/lean): add "hole_commands" server command
|
2017-06-14 22:16:34 -07:00 |
|
hole_command.h
|
chore(library/tactic/hole_command,frontends/lean/interactive): fix style
|
2017-06-14 22:23:25 -07:00 |
|
hsubstitution.cpp
|
|
|
|
hsubstitution.h
|
|
|
|
induction_tactic.cpp
|
feat(library/type_context): use context_cache interface
|
2018-02-21 15:04:20 -08:00 |
|
induction_tactic.h
|
|
|
|
init_module.cpp
|
feat(library/tactic): add hole_command bookkeeping
|
2017-06-13 21:12:29 -07:00 |
|
init_module.h
|
|
|
|
intro_tactic.cpp
|
chore(library): use type_context to update metavar_context
|
2018-02-27 12:23:26 -08:00 |
|
intro_tactic.h
|
feat(library/tactic/induction_tactic): new name generator for induction and cases tactics
|
2017-12-05 14:57:36 -08:00 |
|
kabstract.cpp
|
feat(library/init/meta): add support for new unify at rw tactic
|
2018-01-04 13:05:55 -08:00 |
|
kabstract.h
|
feat(library/init/meta): add support for new unify at rw tactic
|
2018-01-04 13:05:55 -08:00 |
|
match_tactic.cpp
|
refactor(library/init/meta/match_tactic): cleanup match_tactic interface
|
2017-12-06 12:52:41 -08:00 |
|
match_tactic.h
|
|
|
|
norm_num_tactic.cpp
|
|
|
|
norm_num_tactic.h
|
|
|
|
occurrences.cpp
|
|
|
|
occurrences.h
|
|
|
|
revert_tactic.cpp
|
fix(library/tactic/revert_tactic): missing catch
|
2018-02-23 12:26:18 -08:00 |
|
revert_tactic.h
|
feat(library/type_context): use context_cache interface
|
2018-02-21 15:04:20 -08:00 |
|
rewrite_tactic.cpp
|
feat(library/tactic): use new cache
|
2018-02-21 15:04:20 -08:00 |
|
rewrite_tactic.h
|
feat(library/init/meta/rewrite_tactic): improve rewrite tactic
|
2017-06-30 12:03:27 -07:00 |
|
simp_lemmas.cpp
|
fix(library/tactic/simp_lemmas): avoid rewrite failure with more robust code
|
2018-02-27 10:59:51 -08:00 |
|
simp_lemmas.h
|
feat(library/tactic/simp_tactic): improve mk_simp_attr
|
2018-01-16 16:47:30 -08:00 |
|
simp_result.cpp
|
|
|
|
simp_result.h
|
feat(library/init/meta/simp_tactic): add option for reducing [reducible] definitions at dsimp, and to_unfold : list name similar to the one in the simp tactic
|
2017-07-03 13:28:46 -07:00 |
|
simp_util.h
|
fix(library/tactic/simp_lemmas): avoid rewrite failure with more robust code
|
2018-02-27 10:59:51 -08:00 |
|
simplify.cpp
|
refactor(library): mk_result/get_result_* ~> mk_success/get_success_*
|
2018-03-01 14:56:01 +01:00 |
|
simplify.h
|
fix(library/tactic/simp_lemmas): avoid rewrite failure with more robust code
|
2018-02-27 10:59:51 -08:00 |
|
subst_tactic.cpp
|
fix(library/tactic/subst_tactic): subst was creating type incorrect motive when using dependent elimination
|
2018-02-26 14:02:10 -08:00 |
|
subst_tactic.h
|
|
|
|
tactic_evaluator.cpp
|
feat(frontends/lean,shell/server): "hole" command
|
2017-06-14 21:56:17 -07:00 |
|
tactic_evaluator.h
|
chore(library/vm/interaction_state): do not profile calls into Lean other than tactic execution
|
2018-02-19 09:13:24 -08:00 |
|
tactic_state.cpp
|
refactor(library): mk_result/get_result_* ~> mk_success/get_success_*
|
2018-03-01 14:56:01 +01:00 |
|
tactic_state.h
|
fix(tactic): build on MSVC
|
2018-02-28 10:38:50 -08:00 |
|
unfold_tactic.cpp
|
refactor(library/init/meta/simp_tactic): make sure dunfold tactics use name convention used at simp, dsimp, ...
|
2017-07-03 21:36:17 -07:00 |
|
unfold_tactic.h
|
|
|
|
user_attribute.cpp
|
refactor(library): mk_result/get_result_* ~> mk_success/get_success_*
|
2018-03-01 14:56:01 +01:00 |
|
user_attribute.h
|
refactor(library/tactic/user_attribute,init/meta/attribute): merge caching_user_attribute into user_attribute
|
2017-09-05 23:14:34 +02:00 |
|
vm_monitor.cpp
|
feat(library/tactic, frontends/lean): replace a few mk_tagged_fresh_name with mk_unused_name
|
2018-02-21 15:04:19 -08:00 |
|
vm_monitor.h
|
|
|
