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 |
|
Leonardo de Moura
|
d41bff8c43
|
feat(library): add helper function
|
2015-05-18 09:16:07 -07:00 |
|
Jeremy Avigad
|
18742e8ab8
|
feat(extras/latex/*): add listings style definition and instructions
|
2015-05-17 20:13:57 +10:00 |
|
Jeremy Avigad
|
566acf4b31
|
feat(library/data/finset/card.lean): add card_Union_of_disjoint and other theorems
|
2015-05-17 19:06:10 +10:00 |
|
Jeremy Avigad
|
6549940c63
|
feat(library/data/finset/bigops.lean): add Union for finsets
|
2015-05-17 17:50:32 +10:00 |
|
Jeremy Avigad
|
783dd61083
|
feat(library/data/finset/basic.lean): add useful calculation rules for quantifiers
|
2015-05-17 17:49:02 +10:00 |
|
Jeremy Avigad
|
9720d84095
|
refactor(library/algebra/group_bigops.lean,library/data/nat/bigops.lean): add ext principle, clean up file
|
2015-05-17 16:00:38 +10:00 |
|
Jeremy Avigad
|
4764f6e8ec
|
refactor(library/algebra/group_bigops.lean,library/data/nat/bigops.lean): simplify naming scheme for bigops
|
2015-05-17 15:24:37 +10:00 |
|
Jeremy Avigad
|
6dc1cfca3c
|
feat(library/init/nat.lean): add notation <= and >= for nat
|
2015-05-17 12:57:48 +10:00 |
|
Jeremy Avigad
|
7bde8193fe
|
feat(library/algebra/order): add alternate names for le.antisymm etc.
|
2015-05-17 12:54:36 +10:00 |
|
Jeremy Avigad
|
981bf93ce0
|
feat(library/data/default.lean): add rat and vector
|
2015-05-17 12:19:47 +10:00 |
|