Leonardo de Moura
|
d59410cc41
|
refactor(kernel): support only proof irrelevant mode
|
2016-09-27 17:18:52 -07:00 |
|
Leonardo de Moura
|
cf30d31024
|
fix(library/tactic/cases_tactic): missing case
|
2016-09-12 17:41:22 -07:00 |
|
Leonardo de Moura
|
75155c3824
|
fix(library/tactic/cases_tactic): missing normalization
|
2016-09-06 18:46:14 -07:00 |
|
Leonardo de Moura
|
6c80f7b75c
|
feat(library/tactic/cases_tactic): normalize type
|
2016-09-04 17:18:50 -07:00 |
|
Leonardo de Moura
|
78f81034c6
|
feat(library): add helper methods
|
2016-08-29 08:31:33 -07:00 |
|
Leonardo de Moura
|
b317d4bc58
|
refactor(library/tactic): add hsubstitution module
|
2016-08-29 08:19:05 -07:00 |
|
Leonardo de Moura
|
1a675d69fc
|
refactor(library/tactic/induction_tactic,library/tactic/cases_tactic): replace name_map<name> with substitutions at induction_tactic
This commit also removes dead code from cases_tactic
|
2016-08-28 14:09:22 -07:00 |
|
Leonardo de Moura
|
206bf613d5
|
feat(library/tactic/subst_tactic): use substitutions instead of name_map<name> in the subst_tactic (low level) API
|
2016-08-28 13:29:44 -07:00 |
|
Leonardo de Moura
|
f0f9880ece
|
refactor(library/equations_compiler/elim_match,library/tactic/cases_tactic):
new design for elim_match
I still need to fix lemma generation, and refactor induction/subst tactics
|
2016-08-28 13:15:10 -07:00 |
|
Leonardo de Moura
|
af7060b46e
|
chore(library/tactic/cases_tactic): add trace
|
2016-08-28 07:57:20 -07:00 |
|
Leonardo de Moura
|
95e8228e8a
|
refactor(library/tactic/cases_tactic): improve low-level API
|
2016-08-25 16:34:40 -07:00 |
|
Leonardo de Moura
|
98aefca014
|
fix(library/local_context): depends_on should take into account assigned metavariables
|
2016-08-25 13:49:54 -07:00 |
|
Leonardo de Moura
|
1ea3bc1683
|
fix(library/tactic/cases_tactic): lowlevel interface that gives access to renamed/introduced hypotheses
|
2016-08-21 15:55:56 -07:00 |
|
Leonardo de Moura
|
cda29ea107
|
fix(library/tactic/cases_tactic): incorrect mk_app
|
2016-07-20 09:32:12 -04:00 |
|
Leonardo de Moura
|
fd068344a6
|
feat(library/tactic/cases_tactic): merge method
The renaming tables are essential for implementing the new definitional package.
|
2016-07-15 13:56:17 -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
|
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
|
a5307a34bc
|
feat(library/tactic): add 'cases' tactic skeleton
|
2016-07-12 14:05:03 -04:00 |
|