| .. |
|
backward
|
chore(library/vm,library/tactic): fix warnings produced by the new clang++
|
2016-09-25 11:14:28 -07:00 |
|
simplifier
|
refactor(library/tactic/simp_lemmas_tactics): consistent naming
|
2016-10-09 09:37:20 -07:00 |
|
ac_tactics.cpp
|
|
|
|
ac_tactics.h
|
|
|
|
app_builder_tactics.cpp
|
|
|
|
app_builder_tactics.h
|
|
|
|
apply_tactic.cpp
|
|
|
|
apply_tactic.h
|
|
|
|
assert_tactic.cpp
|
|
|
|
assert_tactic.h
|
|
|
|
cases_tactic.cpp
|
refactor(kernel): support only proof irrelevant mode
|
2016-09-27 17:18:52 -07:00 |
|
cases_tactic.h
|
refactor(library/tactic): add hsubstitution module
|
2016-08-29 08:19:05 -07:00 |
|
change_tactic.cpp
|
|
|
|
change_tactic.h
|
|
|
|
clear_tactic.cpp
|
fix(library/local_context): depends_on should take into account assigned metavariables
|
2016-08-25 13:49:54 -07:00 |
|
clear_tactic.h
|
|
|
|
CMakeLists.txt
|
fix(library/tactic/dsimplify): bugs and implement dsimp using new dsimplify
|
2016-10-12 08:33:40 -07:00 |
|
congr_lemma_tactics.cpp
|
|
|
|
congr_lemma_tactics.h
|
|
|
|
dsimplify.cpp
|
fix(library/tactic/dsimplify): bugs and implement dsimp using new dsimplify
|
2016-10-12 08:33:40 -07:00 |
|
dsimplify.h
|
fix(library/tactic/dsimplify): bugs and implement dsimp using new dsimplify
|
2016-10-12 08:33:40 -07:00 |
|
elaborate.cpp
|
feat(frontends/lean/begin_end_block): add basic auto-quotation
|
2016-09-25 17:03:12 -07:00 |
|
elaborate.h
|
|
|
|
eval.cpp
|
feat(library/tactic/eval): eval_expr for arbitrary expressions
|
2016-10-03 19:01:22 -07:00 |
|
eval.h
|
feat(library/tactic): 'eval_expr' tactic skeleton
|
2016-10-03 16:26:28 -07:00 |
|
exact_tactic.cpp
|
|
|
|
exact_tactic.h
|
|
|
|
fun_info_tactics.cpp
|
|
|
|
fun_info_tactics.h
|
|
|
|
generalize_tactic.cpp
|
|
|
|
generalize_tactic.h
|
|
|
|
gexpr.cpp
|
|
|
|
gexpr.h
|
|
|
|
hsubstitution.cpp
|
refactor(library/tactic): add hsubstitution module
|
2016-08-29 08:19:05 -07:00 |
|
hsubstitution.h
|
refactor(library/tactic): add hsubstitution module
|
2016-08-29 08:19:05 -07:00 |
|
induction_tactic.cpp
|
feat(src/library/inductive_compiler): support for nested inductive types
|
2016-09-16 12:50:59 -07:00 |
|
induction_tactic.h
|
refactor(library/tactic): add hsubstitution module
|
2016-08-29 08:19:05 -07:00 |
|
init_module.cpp
|
fix(library/tactic/dsimplify): bugs and implement dsimp using new dsimplify
|
2016-10-12 08:33:40 -07:00 |
|
init_module.h
|
|
|
|
intro_tactic.cpp
|
feat(library/tactic/intro_tactic): use get_unused_name
|
2016-09-19 16:38:03 -07:00 |
|
intro_tactic.h
|
|
|
|
kabstract.cpp
|
feat(util/rb_map): add unsigned_map
|
2016-10-03 16:26:58 -07:00 |
|
kabstract.h
|
|
|
|
match_tactic.cpp
|
|
|
|
match_tactic.h
|
|
|
|
occurrences.cpp
|
|
|
|
occurrences.h
|
|
|
|
rename_tactic.cpp
|
|
|
|
rename_tactic.h
|
|
|
|
revert_tactic.cpp
|
fix(library/local_context): depends_on should take into account assigned metavariables
|
2016-08-25 13:49:54 -07:00 |
|
revert_tactic.h
|
|
|
|
rewrite_tactic.cpp
|
feat(library/tactic/rewrite_tactic): improve error message
|
2016-09-28 21:17:57 -07:00 |
|
rewrite_tactic.h
|
|
|
|
simp_lemmas_tactics.cpp
|
refactor(library/tactic/simp_lemmas_tactics): consistent naming
|
2016-10-09 09:37:20 -07:00 |
|
simp_lemmas_tactics.h
|
refactor(library/tactic): use new simp_lemmas module in the simplifier
|
2016-10-08 21:54:34 -07:00 |
|
simp_result.cpp
|
|
|
|
simp_result.h
|
|
|
|
subst_tactic.cpp
|
feat(library): add helper methods
|
2016-08-29 08:31:33 -07:00 |
|
subst_tactic.h
|
refactor(library/tactic): add hsubstitution module
|
2016-08-29 08:19:05 -07:00 |
|
tactic_state.cpp
|
feat(library/tactic): expose new dsimplify in Lean
|
2016-10-12 07:25:09 -07:00 |
|
tactic_state.h
|
feat(library/tactic): expose new dsimplify in Lean
|
2016-10-12 07:25:09 -07:00 |
|
unfold_tactic.cpp
|
refactor(library): rename pr1/pr2 ==> fst/snd
|
2016-09-21 09:48:39 -07:00 |
|
unfold_tactic.h
|
|
|
|
user_attribute.cpp
|
feat(library/init/meta/attribute, library/tactic/user_attribute): make sure caching_user_attribute is in (Type 1)
|
2016-10-04 02:05:34 -07:00 |
|
user_attribute.h
|
refactor(library): move user_attribute to tactic folder
|
2016-08-26 09:28:42 -07:00 |
