Leonardo de Moura
60d3255577
fix(library/type_context): issue #1258 again
...
This is yet another fix.
2016-12-22 10:51:16 -08:00
Leonardo de Moura
49e296dee2
fix(library/type_context, library/tactic/induction_tactic): fix for issue #1258 was incorrect
...
The fix was incorrect because it could produce an invalid local context.
Actually, the regression tests/lean/run/1258.lean was producing an
assertion violation.
2016-12-21 21:13:29 -08:00
Leonardo de Moura
9d52b6607d
feat(library/tactic): use annotated_head_beta_reduce instead of head_beta_reduce in tactics
2016-11-21 15:40:12 -08:00
Daniel Selsam
52f87760d8
feat(src/library/inductive_compiler): support for nested inductive types
2016-09-16 12:50:59 -07:00
Leonardo de Moura
f3d2a9f1e4
feat(library/tactic/induction_tactic): improve error messages
2016-09-06 18:39:42 -07:00
Leonardo de Moura
e8397681a5
fix(library/tactic/induction_tactic): normalize type in the induction tactic
2016-09-04 17:36:26 -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
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
af9114d7c9
refactor(library/tactic/induction_tactic): low level induction tactic for internal use
2016-07-14 16:04:05 -04:00
Leonardo de Moura
b390521b30
feat(library/tactic/induction_tactic): clear major premise
2016-07-07 07:39:25 -07:00
Leonardo de Moura
925d538337
chore(library/tactic/induction_tactic): uniform error messages
2016-07-07 07:39:25 -07:00
Leonardo de Moura
dbbe070060
feat(library/tactic): add 'induction' tactic
2016-07-05 19:13:23 -07:00
Leonardo de Moura
aeee79da2b
chore(library): library/tactic => library/old_tactic
2016-06-06 16:38:27 -07:00
Leonardo de Moura
8dde1489f9
refactor(library/util): isolate util procedures that depend on old_type_checker
2016-03-21 13:36:08 -07:00
Leonardo de Moura
29ad781ec2
refactor(kernel): remove converter class
...
This abstraction is not useful after refactoring.
2016-03-19 15:58:15 -07:00
Leonardo de Moura
d8079aa16a
refactor(library): create copy of the kernel type_checker in library
...
Motivation: it will allow us to simplify the kernel type_checker and
make sure it implements the same API provided by type_context
2016-03-18 14:34:10 -07:00
Leonardo de Moura
632d4fae36
chore(library): rename local_context to old_local_context
2016-02-11 18:15:16 -08:00
Leonardo de Moura
c9e9fee76a
refactor(*): remove name_generator and use simpler mk_fresh_name
2016-02-11 18:05:57 -08:00
Leonardo de Moura
7b29ee1666
fix(library/tactic/induction_tactic): fixes #892
2015-12-10 10:52:57 -08:00
Leonardo de Moura
8b3cbb8fdd
fix(library/tactic/induction_tactic): apply substitution to hypothesis type (it may contain metavars)
...
closes #876
2015-12-10 10:11:55 -08:00
Leonardo de Moura
c9ff175cf4
fix(library/tactic/induction_tactic): fixes #893
2015-12-10 10:11:55 -08:00
Leonardo de Moura
6a36bffe4b
fix(library/class_instance_resolution): bugs in new type class resolution procedure
2015-11-08 14:04:57 -08:00
Leonardo de Moura
1b864a838f
fix(library/tactic/induction_tactic.cpp): condition for checking whether 'induction' tatic is applicable or not
...
fixes #690
2015-06-28 13:07:02 -07:00
Leonardo de Moura
5687c24944
refactor(library/tactic/induction_tactic): cleanup
2015-06-22 10:23:54 -07:00
Leonardo de Moura
d547698a56
refactor(library,library/tactic): move class_instance_synth to library
...
This module will be needed by the simplifier
2015-06-01 16:30:40 -07:00
Leonardo de Moura
ca110012d8
feat(library/tactic): automate "generalize-intro-induction/cases" idiom
...
closes #645
2015-05-30 21:57:28 -07:00
Leonardo de Moura
b83b0c0017
fix(library/tactic/induction_tactic): fixes #619
2015-05-21 18:22:07 -07:00
Leonardo de Moura
2b4233ee8e
fix(library/tactic/induction_tactic): exception handling
2015-05-21 10:15:49 -07:00
Leonardo de Moura
d6b72ef4d7
feat(library/tactic/induction_tactic): try available recursors until one works
...
closes #615
2015-05-20 23:23:05 -07:00
Leonardo de Moura
2164ba6f20
fix(library/tactic/induction_tactic): fixes #614
2015-05-20 23:14:11 -07:00
Leonardo de Moura
51d4644832
fix(library/tactic/induction_tactic): fixes #613
2015-05-20 22:26:50 -07:00
Leonardo de Moura
5508e4b132
feat(library/tactic/induction_tactic): type class inference for minor premises
...
closes #611
2015-05-20 20:48:33 -07:00
Leonardo de Moura
029f374a69
fix(library/tactic/induction_tactic): fixes #610
2015-05-20 20:28:02 -07:00
Leonardo de Moura
3e87f09d78
feat(library/tactic/induction_tactic): add support for user-defined recursors that contain parameters that should be synthesized by type class resolution
2015-05-19 15:33:46 -07:00
Leonardo de Moura
78ee055de8
feat(library/tactic): add induction tactic with support for user defined recursors
...
closes #483
closes #492
2015-05-19 13:27:17 -07:00
Leonardo de Moura
b1ece388a6
feat(frontends/lean,library/tactic/induction_tactic): improve induction tactic notation, expand induction tactic implementation
2015-05-18 09:25:07 -07:00
Leonardo de Moura
065a1f7501
feat(library/tactic): add 'induction' tactic skeleton
2015-05-12 20:21:25 -07:00
