| .. |
|
backward
|
|
|
|
smt
|
feat(library/tactic/smt/congruence_closure): add builtin support for (@ne A a b)
|
2017-05-26 17:06:22 -07:00 |
|
ac_tactics.cpp
|
chore(kernel/environment): rename method
|
2017-05-15 14:18:16 -07:00 |
|
ac_tactics.h
|
|
|
|
algebraic_normalizer.cpp
|
feat(library/tactic): start algebraic normalizer
|
2017-05-15 21:46:19 -07:00 |
|
algebraic_normalizer.h
|
feat(library/tactic): start algebraic normalizer
|
2017-05-15 21:46:19 -07:00 |
|
app_builder_tactics.cpp
|
|
|
|
app_builder_tactics.h
|
|
|
|
apply_tactic.cpp
|
chore(library/tactic): make sure "pattern" is the first argument of is_def_eq
|
2017-04-25 09:59:04 -07:00 |
|
apply_tactic.h
|
|
|
|
assert_tactic.cpp
|
|
|
|
assert_tactic.h
|
|
|
|
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
|
fix(library/equations_compiler/elim_match): skip nonvar + inaccessible
|
2017-03-21 08:08:36 -07:00 |
|
change_tactic.cpp
|
|
|
|
change_tactic.h
|
|
|
|
clear_tactic.cpp
|
fix(library/tactic/subst_tactic): fixes #1467
|
2017-03-17 19:54:35 -07:00 |
|
clear_tactic.h
|
|
|
|
CMakeLists.txt
|
refactor(library/tactic,frontends/lean): move tactic_evaluator to library/tactic
|
2017-05-23 15:30:31 -07:00 |
|
congr_lemma_tactics.cpp
|
|
|
|
congr_lemma_tactics.h
|
|
|
|
destruct_tactic.cpp
|
|
|
|
destruct_tactic.h
|
|
|
|
dsimplify.cpp
|
fix(library/tactic/dsimplify): fixes #1603
|
2017-05-25 11:21:06 -07:00 |
|
dsimplify.h
|
feat(library/tactic/dsimplify): replace assigned metavariables
|
2017-04-02 12:49:29 -07:00 |
|
elaborate.cpp
|
feat(library/tactic/elaborator_exception): show context of failed placeholders
|
2017-03-27 13:42:08 -07:00 |
|
elaborate.h
|
|
|
|
elaborator_exception.cpp
|
feat(frontends/lean/elaborator,library/sorry): suppress error message that mention synthetic sorrys
|
2017-05-23 11:14:30 -07:00 |
|
elaborator_exception.h
|
feat(frontends/lean/elaborator,library/sorry): suppress error message that mention synthetic sorrys
|
2017-05-23 11:14:30 -07:00 |
|
eqn_lemmas.cpp
|
fix(library/tactic/eqn_lemmas): fix get_eqn_lemmas_for
|
2017-05-23 20:39:27 -07:00 |
|
eqn_lemmas.h
|
|
|
|
eval.cpp
|
fix(library/tactic/eval,kernel/kernel_exception): hide internal definition name on eval_expr type error
|
2017-03-27 13:42:08 -07:00 |
|
eval.h
|
|
|
|
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
|
|
|
|
hsubstitution.h
|
|
|
|
induction_tactic.cpp
|
fix(library/type_context): fixes #1500
|
2017-03-31 19:19:44 -07:00 |
|
induction_tactic.h
|
|
|
|
init_module.cpp
|
feat(library/tactic): start algebraic normalizer
|
2017-05-15 21:46:19 -07: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
|
chore(library/inductive_compiler/nested.cpp): prove all theorems in C++
|
2017-05-04 16:34:32 -07:00 |
|
kabstract.cpp
|
feat(library/tactic): add options trace.rewrite and trace.kabstract for debugging rewrite tactic
|
2017-03-27 18:18:20 -07:00 |
|
kabstract.h
|
|
|
|
match_tactic.cpp
|
|
|
|
match_tactic.h
|
|
|
|
norm_num_tactic.cpp
|
|
|
|
norm_num_tactic.h
|
|
|
|
occurrences.cpp
|
|
|
|
occurrences.h
|
|
|
|
revert_tactic.cpp
|
fix(library/type_context): fixes #1500
|
2017-03-31 19:19:44 -07:00 |
|
revert_tactic.h
|
fix(library/type_context): fixes #1500
|
2017-03-31 19:19:44 -07:00 |
|
rewrite_tactic.cpp
|
fix(library/tactic/rewrite_tactic): instantiate assign metavars before rewriting
|
2017-05-18 10:57:03 -07:00 |
|
rewrite_tactic.h
|
|
|
|
simp_lemmas.cpp
|
feat(library): instances are not reducible by default anymore
|
2017-04-26 14:10:11 -07:00 |
|
simp_lemmas.h
|
|
|
|
simp_result.cpp
|
|
|
|
simp_result.h
|
|
|
|
simplify.cpp
|
fix(library/tactic/simplify): instantiate assigned metavariables in the simplifier
|
2017-05-18 10:52:11 -07:00 |
|
simplify.h
|
feat(library/tactic/simplify): add eta := tt to simp
|
2017-03-27 17:38:40 -07:00 |
|
subst_tactic.cpp
|
fix(library/type_context): fixes #1500
|
2017-03-31 19:19:44 -07:00 |
|
subst_tactic.h
|
chore(library/inductive_compiler/nested.cpp): prove all theorems in C++
|
2017-05-04 16:34:32 -07:00 |
|
tactic_evaluator.cpp
|
refactor(library/tactic,frontends/lean): move tactic_evaluator to library/tactic
|
2017-05-23 15:30:31 -07:00 |
|
tactic_evaluator.h
|
refactor(library/tactic,frontends/lean): move tactic_evaluator to library/tactic
|
2017-05-23 15:30:31 -07:00 |
|
tactic_state.cpp
|
chore(library/inductive_compiler/nested.cpp): prove all theorems in C++
|
2017-05-04 16:34:32 -07:00 |
|
tactic_state.h
|
|
|
|
unfold_tactic.cpp
|
|
|
|
unfold_tactic.h
|
|
|
|
user_attribute.cpp
|
refactor(frontends/lean/{elaborator,structure_cmd}): compile structure inheritance to nested fields
|
2017-04-24 19:35:15 +02:00 |
|
user_attribute.h
|
|
|
|
vm_monitor.cpp
|
fix(library/tactic/vm_monitor): compilation warning
|
2017-03-22 07:40:16 -07:00 |
|
vm_monitor.h
|
|
|
