| .. |
|
backward
|
chore(frontends/lean,library/tactic): remove old tactic_state functions
|
2017-02-17 15:41:58 +01:00 |
|
smt
|
fix(library/tactic/smt/congruence_closure): relation used to implement congruence tables was not transitive
|
2017-03-17 16:04:41 -07:00 |
|
ac_tactics.cpp
|
fix(library/tactic/ac_tactics): allow nested ac_app macros in perm_ac macro
|
2017-03-08 13:46:49 -08:00 |
|
ac_tactics.h
|
fix(library/module): deadlock?
|
2016-12-29 17:56:50 -08:00 |
|
app_builder_tactics.cpp
|
chore(frontends/lean,library/tactic): remove old tactic_state functions
|
2017-02-17 15:41:58 +01:00 |
|
app_builder_tactics.h
|
|
|
|
apply_tactic.cpp
|
chore(frontends/lean,library/tactic): remove old tactic_state functions
|
2017-02-17 15:41:58 +01:00 |
|
apply_tactic.h
|
|
|
|
assert_tactic.cpp
|
chore(frontends/lean,library/tactic): remove old tactic_state functions
|
2017-02-17 15:41:58 +01:00 |
|
assert_tactic.h
|
feat(library/init/meta/smt_tactic): add assert/assertv/define/definev/pose/note for smt_tactic
|
2017-01-03 17:12:00 -08:00 |
|
cases_tactic.cpp
|
fix(library/tactic): we should preserve names when using the revert/do_something/intro idiom
|
2017-03-11 12:20:39 -08:00 |
|
cases_tactic.h
|
feat(library/tactic/cases_tactic): add support for generalized inductive datatypes at 'cases' tactic
|
2017-03-06 11:49:04 -08:00 |
|
change_tactic.cpp
|
chore(frontends/lean,library/tactic): remove old tactic_state functions
|
2017-02-17 15:41:58 +01:00 |
|
change_tactic.h
|
feat(library/init/meta): smt_tactic skeleton
|
2016-12-31 18:22:23 -08:00 |
|
clear_tactic.cpp
|
fix(library/tactic/subst_tactic): fixes #1467
|
2017-03-17 19:54:35 -07:00 |
|
clear_tactic.h
|
fix(library/type_context, library/tactic/induction_tactic): fix for issue #1258 was incorrect
|
2016-12-21 21:13:29 -08:00 |
|
CMakeLists.txt
|
fix(frontends/lean, library/tactic): error position in auto quoted terms
|
2017-02-09 18:03:04 -08:00 |
|
congr_lemma_tactics.cpp
|
chore(frontends/lean,library/tactic): remove old tactic_state functions
|
2017-02-17 15:41:58 +01:00 |
|
congr_lemma_tactics.h
|
|
|
|
destruct_tactic.cpp
|
chore(frontends/lean,library/tactic): remove old tactic_state functions
|
2017-02-17 15:41:58 +01:00 |
|
destruct_tactic.h
|
feat(library/tactic): add destruct tactic that is similar to cases, but does not use revert/intro/clear
|
2016-12-30 17:05:24 -08:00 |
|
dsimplify.cpp
|
chore(frontends/lean,library/tactic): remove old tactic_state functions
|
2017-02-17 15:41:58 +01:00 |
|
dsimplify.h
|
fix(library/tactic/smt/hinst_lemmas): pattern normalization issue
|
2017-01-08 23:35:39 -08:00 |
|
elaborate.cpp
|
chore(frontends/lean,library/tactic): remove old tactic_state functions
|
2017-02-17 15:41:58 +01:00 |
|
elaborate.h
|
feat(library/tactic): store name of current declaration in tactic_state
|
2017-01-28 08:27:19 +01:00 |
|
elaborator_exception.cpp
|
refactor(*): reduce exception context info from expr to pos_info
|
2017-02-17 13:45:57 +01:00 |
|
elaborator_exception.h
|
refactor(*): reduce exception context info from expr to pos_info
|
2017-02-17 13:45:57 +01:00 |
|
eqn_lemmas.cpp
|
chore(frontends/lean,library/tactic): remove old tactic_state functions
|
2017-02-17 15:41:58 +01:00 |
|
eqn_lemmas.h
|
feat(library/tactic/smt/smt_state): add tactic for adding equational lemmas for a definition
|
2017-01-05 15:47:58 -08:00 |
|
eval.cpp
|
fix(library/tactic/eval): make sure old position information nested in the expression being evaluated is not used in type error messages
|
2017-02-26 22:38:24 -08:00 |
|
eval.h
|
feat(library/tactic): 'eval_expr' tactic skeleton
|
2016-10-03 16:26:28 -07:00 |
|
exact_tactic.cpp
|
chore(frontends/lean,library/tactic): remove old tactic_state functions
|
2017-02-17 15:41:58 +01:00 |
|
exact_tactic.h
|
|
|
|
fun_info_tactics.cpp
|
chore(frontends/lean,library/tactic): remove old tactic_state functions
|
2017-02-17 15:41:58 +01:00 |
|
fun_info_tactics.h
|
|
|
|
generalize_tactic.cpp
|
chore(frontends/lean,library/tactic): remove old tactic_state functions
|
2017-02-17 15:41:58 +01:00 |
|
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
|
fix(library/tactic): we should preserve names when using the revert/do_something/intro idiom
|
2017-03-11 12:20:39 -08:00 |
|
induction_tactic.h
|
refactor(library/tactic): add hsubstitution module
|
2016-08-29 08:19:05 -07:00 |
|
init_module.cpp
|
feat(library/tactic): add destruct tactic that is similar to cases, but does not use revert/intro/clear
|
2016-12-30 17:05:24 -08:00 |
|
init_module.h
|
|
|
|
intro_tactic.cpp
|
fix(library/tactic): we should preserve names when using the revert/do_something/intro idiom
|
2017-03-11 12:20:39 -08:00 |
|
intro_tactic.h
|
fix(library/tactic): we should preserve names when using the revert/do_something/intro idiom
|
2017-03-11 12:20:39 -08:00 |
|
kabstract.cpp
|
fix(library/tactic/kabstract.cpp): only use replace_fn cache if replacing all occs
|
2017-03-15 19:40:52 -07:00 |
|
kabstract.h
|
|
|
|
match_tactic.cpp
|
feat(library/tactic/match_tactic): return also assignments for universe meta-variables
|
2017-02-17 20:08:09 -08:00 |
|
match_tactic.h
|
|
|
|
norm_num_tactic.cpp
|
chore(frontends/lean,library/tactic): remove old tactic_state functions
|
2017-02-17 15:41:58 +01:00 |
|
norm_num_tactic.h
|
feat(library/tactic): add norm_num_tactic
|
2016-12-17 16:48:40 -08:00 |
|
occurrences.cpp
|
|
|
|
occurrences.h
|
|
|
|
rename_tactic.cpp
|
chore(frontends/lean,library/tactic): remove old tactic_state functions
|
2017-02-17 15:41:58 +01:00 |
|
rename_tactic.h
|
|
|
|
revert_tactic.cpp
|
chore(frontends/lean,library/tactic): remove old tactic_state functions
|
2017-02-17 15:41:58 +01:00 |
|
revert_tactic.h
|
|
|
|
rewrite_tactic.cpp
|
chore(frontends/lean,library/tactic): remove old tactic_state functions
|
2017-02-17 15:41:58 +01:00 |
|
rewrite_tactic.h
|
|
|
|
simp_lemmas.cpp
|
chore(frontends/lean,library/tactic): remove old tactic_state functions
|
2017-02-17 15:41:58 +01:00 |
|
simp_lemmas.h
|
feat(library/init/meta/smt_tactic): allow user to select simp attribute to be used during SMT preprocessing, use preprocessing at intros too
|
2017-01-01 22:26:26 -08:00 |
|
simp_result.cpp
|
|
|
|
simp_result.h
|
|
|
|
simplify.cpp
|
feat(library/tactic/simplify): relax reducibility constraints when matching implicit arguments
|
2017-03-08 20:08:54 -08:00 |
|
simplify.h
|
refactor(library/tactic, library/init/meta): simplify_config => simp_config
|
2017-02-19 13:10:36 -08:00 |
|
subst_tactic.cpp
|
fix(library/tactic/subst_tactic): fixes #1467
|
2017-03-17 19:54:35 -07:00 |
|
subst_tactic.h
|
feat(inductive_compiler): generate injectivity lemmas
|
2017-03-10 22:27:18 -08:00 |
|
tactic_state.cpp
|
chore(library/init/meta): add head prefix to head reduction tactics, and add zeta tactic (that applies zeta reduction to all subterms)
|
2017-03-02 10:55:38 -08:00 |
|
tactic_state.h
|
chore(util,kernel,library): clang warnings
|
2017-02-17 20:01:34 -08:00 |
|
unfold_tactic.cpp
|
chore(frontends/lean,library/tactic): remove old tactic_state functions
|
2017-02-17 15:41:58 +01:00 |
|
unfold_tactic.h
|
refactor(library/tactic/unfold_tactic): add dunfold C++ function
|
2017-02-04 16:33:12 -08:00 |
|
user_attribute.cpp
|
refactor(library/tactic/user_attribute): use attribute for registering attributes. naturally.
|
2017-03-15 14:06:34 -07:00 |
|
user_attribute.h
|
feat(library/init/meta/smt_tactic): allow user to select simp attribute to be used during SMT preprocessing, use preprocessing at intros too
|
2017-01-01 22:26:26 -08:00 |
|
vm_monitor.cpp
|
refactor(init/meta,library/vm): use structure for position information
|
2017-02-21 11:06:39 -08:00 |
|
vm_monitor.h
|
feat(library/vm/vm): invoke debugger (aka vm_monitor)
|
2016-11-14 14:45:49 -08:00 |
