Leonardo de Moura
|
dfc834fb5c
|
feat(library/old_tactic/tactic/inversion_tactic): remove dead code
|
2016-07-15 13:56:16 -04:00 |
|
Leonardo de Moura
|
e1a9008d7c
|
feat(library/tactic/cases_tactic): add a list containing the constructor associated with each new goal
|
2016-07-15 13:56:16 -04:00 |
|
Leonardo de Moura
|
031dbcd380
|
feat(library/tactic/cases_tactic): add missing case
|
2016-07-15 13:56:16 -04:00 |
|
Leonardo de Moura
|
8934172ed2
|
feat(library/tactic/cases_tactic): start unify_eqs
|
2016-07-15 13:55:51 -04:00 |
|
Leonardo de Moura
|
2ac7b5afca
|
fix(library/tactic/subst_tactic): typo
|
2016-07-15 13:52:55 -04:00 |
|
Leonardo de Moura
|
de0ae18dd1
|
feat(library/tactic/subst_tactic): add low-level subst tactic for internal use
|
2016-07-14 18:00:29 -04:00 |
|
Leonardo de Moura
|
d9fb21ecc8
|
feat(library/tactic/cases_tactic): clear auxiliary indices
|
2016-07-14 16:54:04 -04:00 |
|
Leonardo de Moura
|
95a103b98b
|
feat(library/tactic/cases_tactic): use 'induction' tactic to implement easy case of 'cases' tactic
|
2016-07-14 16:04:27 -04:00 |
|
Leonardo de Moura
|
af9114d7c9
|
refactor(library/tactic/induction_tactic): low level induction tactic for internal use
|
2016-07-14 16:04:05 -04:00 |
|
Leonardo de Moura
|
d49ab7d220
|
feat(library/tactic/induction_tactic): new flavor of intron
|
2016-07-14 14:51:45 -04:00 |
|
Leonardo de Moura
|
04fe48539f
|
feat(library/tactic/revert_tactic): low level version of 'revert' tactic
|
2016-07-14 14:42:56 -04:00 |
|
Leonardo de Moura
|
a5307a34bc
|
feat(library/tactic): add 'cases' tactic skeleton
|
2016-07-12 14:05:03 -04:00 |
|
Leonardo de Moura
|
394995dff0
|
fix(library/local_context): missing 'const'
|
2016-07-12 13:41:42 -04:00 |
|
Leonardo de Moura
|
558b9153e2
|
chore(library/type_context): remove redundant method
|
2016-07-12 13:02:42 -04:00 |
|
Leonardo de Moura
|
5f2591b3a3
|
feat(library/init/meta/backward): expose back_lemmas (index)
Motivation: the user can create the index once and use it many times.
|
2016-07-10 17:11:24 -07:00 |
|
Leonardo de Moura
|
1c878468ce
|
chore(library/tactic/backward/backward_chaining): fix style
|
2016-07-10 16:26:50 -07:00 |
|
Leonardo de Moura
|
e48fa15b71
|
feat(library/tactic/backward/backward_chaining): add 'pre_tactic' to backward_chaining_core
|
2016-07-10 16:11:13 -07:00 |
|
Leonardo de Moura
|
20de45e9d1
|
chore(library/blast/backward): remove dead code
|
2016-07-10 13:50:51 -07:00 |
|
Leonardo de Moura
|
7c8d0f444f
|
feat(library/tactic/backward): finish backward chaining tactic
|
2016-07-10 13:49:28 -07:00 |
|
Leonardo de Moura
|
af9c7148b3
|
feat(library/tactic/backward): add backward_chaining skeleton tactic
|
2016-07-10 11:45:25 -07:00 |
|
Leonardo de Moura
|
bc9a0701f8
|
refactor(library/tactic/apply_tactic): expose 'apply' tactic for internal use
|
2016-07-10 10:41:02 -07:00 |
|
Leonardo de Moura
|
f79e46a8a0
|
fix(frontends/lean/old_elaborator): remove "old" [intro]
|
2016-07-10 10:39:34 -07:00 |
|
Leonardo de Moura
|
df113de725
|
fix(library/congr_lemma): compilation error in debug mode
|
2016-07-10 10:37:27 -07:00 |
|
Leonardo de Moura
|
2ae516ebe0
|
refactor(library): move backward lemmas to tactic
|
2016-07-10 10:17:56 -07:00 |
|
Leonardo de Moura
|
142f7da03c
|
refactor(library): move gexpr to tactic folder
|
2016-07-10 09:21:05 -07:00 |
|
Leonardo de Moura
|
69cc58dbda
|
fix(library/tactic/clear_tactic): fail if hypothesis has dependecies
|
2016-07-09 17:19:49 -07:00 |
|
Daniel Selsam
|
010c81f8aa
|
chore(simplifier): remove duplicate include statement
|
2016-07-09 10:15:07 -07:00 |
|
Daniel Selsam
|
0742b65183
|
fix(library/metavar_context): comment out problematic assertion
|
2016-07-09 10:14:45 -07:00 |
|
Daniel Selsam
|
237ff5dbf6
|
fix(simplifier): need scope_trace_env when pp-ing exprs with tmp-metavariables
Conflicts:
src/library/tactic/simplifier/simplifier.cpp
|
2016-07-09 10:14:20 -07:00 |
|
Daniel Selsam
|
ea19bb40dd
|
feat(simplifier): detect refl proofs from simp extensions
|
2016-07-09 10:11:58 -07:00 |
|
Daniel Selsam
|
a354973fee
|
chore(simplifier): remove old TODO
|
2016-07-09 10:11:45 -07:00 |
|
Daniel Selsam
|
10773760bc
|
fix(simplifier): need to instantiate mvars in results from simp extensions
|
2016-07-09 10:11:12 -07:00 |
|
Daniel Selsam
|
c3d44249bc
|
feat(simplifier): take list of lemmas and tactic as args to simplify
|
2016-07-09 10:10:59 -07:00 |
|
Leonardo de Moura
|
c49f51dccc
|
perf(library/tactic/simplifier/simplifier): minimize number of check_system invocations
|
2016-07-08 21:53:33 -07:00 |
|
Leonardo de Moura
|
ec4cd87172
|
perf(library/tactic/simplifier/simplifier): avoid instantiate, use 'for' instead of 'for_each'
|
2016-07-08 21:38:16 -07:00 |
|
Leonardo de Moura
|
8a24f06054
|
chore(library/type_context): remove dead code
|
2016-07-08 18:24:22 -07:00 |
|
Leonardo de Moura
|
1f71bc9798
|
feat(library/type_context): simplify on_is_def_eq_failure
|
2016-07-08 18:06:27 -07:00 |
|
Leonardo de Moura
|
519f47c9a7
|
fix(library/type_context): ignore assigned variables
|
2016-07-08 16:50:25 -07:00 |
|
Leonardo de Moura
|
e3df5e83b9
|
feat(library/type_context): cache on_is_def_eq_failure
|
2016-07-08 16:42:46 -07:00 |
|
Leonardo de Moura
|
ce9be907d9
|
perf(library/type_context): cache result of is_aux_recursor predicate
|
2016-07-08 09:25:45 -07:00 |
|
Leonardo de Moura
|
1ae6ce3f9c
|
perf(library/type_context): use expr_struct_map for whnf_cache
|
2016-07-08 09:21:30 -07:00 |
|
Leonardo de Moura
|
f34e84dacb
|
feat(frontends/lean/parser): cute binders
|
2016-07-08 07:50:58 -07:00 |
|
Leonardo de Moura
|
862b535c80
|
perf(library/type_context): cache whnf
|
2016-07-07 22:20:49 -07:00 |
|
Leonardo de Moura
|
d900a1b156
|
feat(library/type_context): faster find_unsynth_metavar
10% performance improvement on
../../tests/lean/perf/perm_ac_commring_50.lean
|
2016-07-07 07:39:26 -07:00 |
|
Leonardo de Moura
|
dce8776cfd
|
refactor(library/fun_info): separate subsingleton information from general param_info
|
2016-07-07 07:39:26 -07:00 |
|
Leonardo de Moura
|
9fb3e0d1e1
|
feat(library/type_context): use equiv_manager
|
2016-07-07 07:39:25 -07:00 |
|
Leonardo de Moura
|
9f8e3752f0
|
feat(kernel/equiv_manager): use expr_struct_map in the equiv_manager
|
2016-07-07 07:39:25 -07:00 |
|
Leonardo de Moura
|
c379783c84
|
chore(library/old_tactic/tactic): remove old code
It has already been ported to new tactic framework.
|
2016-07-07 07:39:25 -07:00 |
|
Leonardo de Moura
|
b390521b30
|
feat(library/tactic/induction_tactic): clear major premise
|
2016-07-07 07:39:25 -07:00 |
|
Leonardo de Moura
|
7b1e67d899
|
feat(library/tactic/clear_tactic): add low-level induction tactic
|
2016-07-07 07:39:25 -07:00 |
|