Leonardo de Moura
|
b83b0c0017
|
fix(library/tactic/induction_tactic): fixes #619
|
2015-05-21 18:22:07 -07:00 |
|
Leonardo de Moura
|
f830bf54c2
|
refactor(*): clarify name_generator ownership
|
2015-05-21 14:32:36 -07:00 |
|
Leonardo de Moura
|
a7ead5fc14
|
fix(library/relation_manager): typo
|
2015-05-21 14:12:28 -07:00 |
|
Leonardo de Moura
|
e3250f0ffd
|
feat(library/simplifier): add conditional equivalence detection
|
2015-05-21 13:55:23 -07:00 |
|
Leonardo de Moura
|
907d017cbf
|
feat(library/relation_manager): cache information about binary relations
|
2015-05-21 13:04:33 -07:00 |
|
Leonardo de Moura
|
c2faa0fe98
|
refactor(library): rename equivalence_manager to relation_manager
|
2015-05-21 12:25:02 -07:00 |
|
Leonardo de Moura
|
2b4233ee8e
|
fix(library/tactic/induction_tactic): exception handling
|
2015-05-21 10:15:49 -07:00 |
|
Leonardo de Moura
|
6a87239a5d
|
chore(kernel/justification): fix compilation warning
|
2015-05-21 10:13:44 -07:00 |
|
Leonardo de Moura
|
76e7f2e7d8
|
feat(kernel/justification): make sure the code does not depend on the argument order of evaluation generated by a compiler
see issue #618
|
2015-05-21 07:42:10 -07:00 |
|
Leonardo de Moura
|
89581cead7
|
fix(frontends/lean/parser): fixes #616
|
2015-05-20 23:33:41 -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
|
2d22bb8ea2
|
feat(frontends/lean/builtin_cmds): do not unfold proofs in the eval command
In the future, we should probably add an option for unfolding proofs.
|
2015-05-20 19:14:57 -07:00 |
|
Leonardo de Moura
|
d5da659be7
|
feat(frontends/lean/elaborator): include overload information in error messages
|
2015-05-20 17:21:27 -07:00 |
|
Leonardo de Moura
|
76c3757db7
|
feat(frontends/lean/elaborator): use custom normalizers for detecting whether there are coercions from/to a given type
closes #547
|
2015-05-20 16:12:12 -07:00 |
|
Leonardo de Moura
|
608984cd4c
|
chore(frontends/lean/elaborator): cleanup ensure fun
|
2015-05-20 15:10:45 -07:00 |
|
Leonardo de Moura
|
af3f0088f4
|
feat(frontends/lean): add 'override' (notation) command
|
2015-05-20 11:42:16 -07:00 |
|
Leonardo de Moura
|
90ea4995f4
|
fix(emacs/lean-syntax): remove deprecated keywords
|
2015-05-19 18:34:14 -07:00 |
|
Leonardo de Moura
|
8ce992b077
|
feat(frontends/lean/builtin_exprs): allow 'obtain' to be used in tactic mode
|
2015-05-19 16:26:02 -07:00 |
|
Leonardo de Moura
|
c133d26505
|
feat(frontends/lean/builtin_exprs): change how 'show' is processed in tactics
Unresolved placeholders were not being reported
|
2015-05-19 16:23:50 -07:00 |
|
Leonardo de Moura
|
1665ee39e8
|
feat(library/data/finset/card): test 'induction' tactic at finset
|
2015-05-19 15:56:51 -07:00 |
|
Leonardo de Moura
|
5f628d5080
|
feat(frontends/lean/builtin_exprs): allow 'calc' expressions to be used in tactic mode
|
2015-05-19 15:54:49 -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
|
5b1491bdbd
|
feat(library/user_recursors): store number of arguments expected by recursor
|
2015-05-19 12:24:46 -07:00 |
|
Leonardo de Moura
|
1e4285cf41
|
fix(library/user_recursors): invalid recursor_info for builtin indexed families
|
2015-05-19 12:19:46 -07:00 |
|
Leonardo de Moura
|
6da2ba331f
|
fix(library/user_recursors): memory access violation
|
2015-05-19 11:07:31 -07:00 |
|
Leonardo de Moura
|
4f12409c63
|
fix(library/unifier): assertion violation
This assertion violation was introduced when we added "projection
macros" to speedup the elaboration process.
|
2015-05-19 10:07:31 -07:00 |
|
Leonardo de Moura
|
937d6ac7b6
|
fix(frontends/lean/pp): print notation produces incorrect output
fixes #604
|
2015-05-19 09:57:13 -07:00 |
|
Leonardo de Moura
|
e1c2340db2
|
fix(frontends/lean): consistent behavior for protected declarations
see https://github.com/leanprover/lean/issues/604#issuecomment-103265608
closes #609
|
2015-05-18 22:35:18 -07:00 |
|
Leonardo de Moura
|
d8bd3c21b5
|
feat(frontends/lean/builtin_cmds): display "protected" for protected declarations in the print command
|
2015-05-18 17:19:34 -07:00 |
|
Leonardo de Moura
|
c53b96c8d3
|
feat(frontends/lean): print all options for overloaded identifier
closes #608
|
2015-05-18 17:14:17 -07:00 |
|
Floris van Doorn
|
1c77122fd0
|
fix(tests): update tests because [unfold-c] attribute has been added to some definitions
|
2015-05-18 15:59:55 -07:00 |
|
Floris van Doorn
|
c430d1d5ba
|
feat(category.constructions): define comma category
|
2015-05-18 15:59:55 -07:00 |
|
Floris van Doorn
|
eedf1992bf
|
feat(functor): prove sorry's, and shorten some proofs
|
2015-05-18 15:59:55 -07:00 |
|
Floris van Doorn
|
6ca9635d53
|
feat(hit.trunc): replace sorry by proof
|
2015-05-18 15:59:55 -07:00 |
|
Floris van Doorn
|
de6294a4ce
|
feat(hott.core): add more files to core.hlean
|
2015-05-18 15:59:55 -07:00 |
|
Floris van Doorn
|
2144036cdb
|
feat(hott.circle): prove that the fundamental group of the circle is equal to the integers, as groups
Also many minor fixes at various places
|
2015-05-18 15:59:55 -07:00 |
|
Floris van Doorn
|
1597337c72
|
feat(path): add unfold-c attribute to definitions
|
2015-05-18 15:59:55 -07:00 |
|
Floris van Doorn
|
17a9bb4bc2
|
fix(types.W): clean-up W file, remove 'exit'
|
2015-05-18 15:59:54 -07:00 |
|
Leonardo de Moura
|
19361f0196
|
feat(library/unifier): do not fire type class resolution as last resort when type contains metavariables
see discussion at #604
|
2015-05-18 15:45:23 -07:00 |
|
Leonardo de Moura
|
1fbc85f6df
|
fix(util/list_fn): add missing file
fixes #606
|
2015-05-18 15:16:29 -07:00 |
|
Leonardo de Moura
|
c61c049152
|
feat(library/user_recursors): generalize acceptable use-defined recursors
see issue #492
|
2015-05-18 14:21:10 -07:00 |
|
Leonardo de Moura
|
62082c72a8
|
fix(library/user_recursors): remove unnecessary restriction on minor premises of user-defined recursors
see issue #492
|
2015-05-18 10:09:11 -07:00 |
|
Leonardo de Moura
|
830d0ce1a7
|
fix(library/user_recursors): make sure homotopy.rec_on is recognized as a valid user-defined recursor
see issue #492
|
2015-05-18 09:57:50 -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
|
4256984803
|
fix(library/tactic/inversion_tactic): incorrect check
|
2015-05-18 09:16:07 -07:00 |
|