lean4-htt/src/library/tactic
2018-08-23 14:54:41 -07:00
..
cases_tactic.cpp chore(library): remove inverse.cpp 2018-08-23 13:16:27 -07:00
cases_tactic.h refactor(*): list<name> ==> obj_list<name> 2018-05-23 15:48:43 -07:00
clear_tactic.cpp refactor(kernel/expr): remove mlocal_* functions 2018-06-22 14:25:31 -07:00
clear_tactic.h
CMakeLists.txt chore(library/tactic): remove tactic/eval.cpp and tactic/gexpr.cpp 2018-08-23 14:54:41 -07:00
elaborate.cpp refactor(kernel/expr): remove mlocal_* functions 2018-06-22 14:25:31 -07:00
elaborate.h
elaborator_exception.cpp refactor(kernel): move formatting stuff out of the kernel 2018-06-07 16:28:54 -07:00
elaborator_exception.h refactor(*): use C++11 std::current_exception and std::rethrow_exception 2018-06-07 16:28:54 -07:00
exact_tactic.cpp chore(library/tactic): remove app_builder_tactics 2018-08-23 14:22:00 -07:00
exact_tactic.h
hsubstitution.cpp refactor(kernel/expr): remove mlocal_* functions 2018-06-22 14:25:31 -07:00
hsubstitution.h
induction_tactic.cpp refactor(kernel/expr): remove mlocal_* functions 2018-06-22 14:25:31 -07:00
induction_tactic.h refactor(*): list<name> ==> obj_list<name> 2018-05-23 15:48:43 -07:00
init_module.cpp chore(library/tactic): remove tactic/eval.cpp and tactic/gexpr.cpp 2018-08-23 14:54:41 -07:00
init_module.h
intro_tactic.cpp refactor(kernel/expr): remove mlocal_* functions 2018-06-22 14:25:31 -07:00
intro_tactic.h refactor(*): list<name> ==> obj_list<name> 2018-05-23 15:48:43 -07:00
kabstract.cpp refactor(kernel/expr): implement expr using runtime/object 2018-06-21 16:05:33 -07:00
kabstract.h refactor(frontends/lean,library/tactic/kabstract): remove add_key_equivalence command 2018-05-30 14:10:03 -07:00
occurrences.cpp
occurrences.h
revert_tactic.cpp refactor(kernel/expr): remove mlocal_* functions 2018-06-22 14:25:31 -07:00
revert_tactic.h feat(library/type_context): use context_cache interface 2018-02-21 15:04:20 -08:00
simp_util.h refactor(kernel): split declaration into declaration and constant_info 2018-08-22 17:53:11 -07:00
subst_tactic.cpp chore(library/tactic): remove app_builder_tactics 2018-08-23 14:22:00 -07:00
subst_tactic.h
tactic_evaluator.cpp chore(kernel): type_checker ==> old_type_checker 2018-06-06 16:10:40 -07:00
tactic_evaluator.h chore(*): type_context ==> type_context_old 2018-03-05 12:38:24 -08:00
tactic_state.cpp chore(library/tactic): remove simp_lemmas 2018-08-23 14:10:36 -07:00
tactic_state.h refactor(*): use C++11 std::current_exception and std::rethrow_exception 2018-06-07 16:28:54 -07:00