Leonardo de Moura
|
9d01868361
|
feat(frontends/lean): use rewrite tactic to implement unfold (it has a unfold step)
closes #502
|
2015-04-24 17:23:12 -07:00 |
|
Leonardo de Moura
|
28404fe16d
|
fix(library/tactic/rewrite_tactic): second problem reported at issue #548
closes #548
|
2015-04-24 16:49:32 -07:00 |
|
Leonardo de Moura
|
4148d6b8cc
|
fix(library/tactic/rewrite_tactic): first two problems at issue #548
|
2015-04-24 16:07:00 -07:00 |
|
Leonardo de Moura
|
6134c8822a
|
fix(frontends/lean/util): assertion violation
fixes #559
|
2015-04-24 15:09:23 -07:00 |
|
Leonardo de Moura
|
f723550d33
|
feat(frontends/lean/elaborator): decorates error message with free variables introduced by the left-hand-side of the equation
closes #528
|
2015-04-24 14:58:15 -07:00 |
|
Leonardo de Moura
|
4a157ee676
|
refactor(kernel/justification): create "wrapper" justification
It allows us to provide a different pretty printer.
This is a cleanup, and also helps to address issue #528
|
2015-04-24 14:49:32 -07:00 |
|
Leonardo de Moura
|
1149ead14c
|
chore(library/logic/examples/colog88): remove unnecessary annotation
|
2015-04-24 12:45:06 -07:00 |
|
Leonardo de Moura
|
a5306e70eb
|
feat(library/logic/examples/negative): add example showing that allowing negative inductive datatypes would lead to inconsistency
|
2015-04-24 09:33:09 -07:00 |
|
Leonardo de Moura
|
15c331591e
|
feat(library/logic/examples/colog88): add example from COLOG-88 paper
|
2015-04-24 09:33:09 -07:00 |
|
Leonardo de Moura
|
8241863abe
|
feat(kernel/hits): add two builtin HITs: type_quotient and trunc
|
2015-04-23 15:32:31 -07:00 |
|
Floris van Doorn
|
591a563be3
|
feat(hit): For all hits, add the elimination to the universe (using ua)
|
2015-04-23 14:29:04 -07:00 |
|
Floris van Doorn
|
f41d92199a
|
feat(hit): make type quotient primitive instead of colimit
|
2015-04-23 14:29:04 -07:00 |
|
Floris van Doorn
|
1d9c17342a
|
feat(hit): define mapping cylinder, coequalizer and quotient in terms of colimit
|
2015-04-23 14:29:04 -07:00 |
|
Floris van Doorn
|
51e87213d0
|
feat(hit): define nondependent recursors for all hits, sequential colimit, and elaborate on spheres
squash
|
2015-04-23 14:29:04 -07:00 |
|
Floris van Doorn
|
ffe158f785
|
feat(hit.suspension): add definition of spheres and the circle
|
2015-04-23 14:29:04 -07:00 |
|
Floris van Doorn
|
2469b8a2f8
|
feat(hott): add primitive hits
|
2015-04-23 14:29:04 -07:00 |
|
Floris van Doorn
|
cb5b07093f
|
fix(arity): remove unnecessary implicit arguments
|
2015-04-23 14:29:04 -07:00 |
|
Soonho Kong
|
c1b23f29c9
|
doc(emacs/README.md): add debian case
[skip ci]
|
2015-04-23 15:05:08 -04:00 |
|
Leonardo de Moura
|
2613e7c444
|
fix(frontends/lean): bug when handling identifiers in tactics
This bug was reported by Jeremy in the Lean Google group:
https://groups.google.com/forum/?utm_medium=email&utm_source=footer#!msg/lean-discuss/ZKJ8WPPEVJA/n05x6rPRzvMJ
|
2015-04-22 16:03:22 -07:00 |
|
Leonardo de Moura
|
e1a609cad9
|
fix(tests/lean/interactive/findp): test output to reflect changes in the stdlib
|
2015-04-22 13:08:56 -07:00 |
|
Floris van Doorn
|
9d805437f0
|
fix(reserved_notation): lower binding power of 'iff'
|
2015-04-22 13:06:11 -07:00 |
|
Floris van Doorn
|
b86ee9dfa6
|
feat(precategory): add composition of nat. trans. with functor
|
2015-04-22 13:06:11 -07:00 |
|
Floris van Doorn
|
a79a3043ed
|
feat(hott/types): a bit of cleanup
|
2015-04-22 13:06:11 -07:00 |
|
Floris van Doorn
|
d4a929febb
|
feat(lean-input): add some notation
|
2015-04-22 13:06:11 -07:00 |
|
Floris van Doorn
|
ee4cba4e0b
|
style(hott): a bit of cleanup
|
2015-04-22 13:06:11 -07:00 |
|
Floris van Doorn
|
17f3ac6ec2
|
fix(hott): fix binding power of 2 notations
|
2015-04-22 13:06:11 -07:00 |
|
Leonardo de Moura
|
349cdb3fe7
|
test(tests/lean): add test showing that the binder type update should not change the parameter order
|
2015-04-22 13:04:05 -07:00 |
|
Leonardo de Moura
|
cdf929d178
|
fix(frontends/lean/local_decls): missing '{}' around macro
|
2015-04-22 12:54:42 -07:00 |
|
Leonardo de Moura
|
a526cd92ac
|
fix(frontends/lean): bug in pretty printer
this is related to issue #530
|
2015-04-22 12:44:08 -07:00 |
|
Leonardo de Moura
|
dc93603b4a
|
feat(frontends/lean): parameter and variable binder type update
see issue #532
|
2015-04-22 12:28:11 -07:00 |
|
Leonardo de Moura
|
91f21c007a
|
feat(frontends/lean): remove 'context' command
|
2015-04-22 11:32:02 -07:00 |
|
Leonardo de Moura
|
53653c3526
|
fix(frontends/lean): pretty printing in sections with parameters
fix #530
|
2015-04-21 22:44:09 -07:00 |
|
Leonardo de Moura
|
caf28f4053
|
fix(frontends/lean/decl_cmds): missing condition
|
2015-04-21 21:08:57 -07:00 |
|
Leonardo de Moura
|
22f6a95cc4
|
feat(frontends/lean): local notation override global one
|
2015-04-21 19:55:59 -07:00 |
|
Leonardo de Moura
|
8e9997e253
|
chore(tests/lean/interactive/sec_info_bug): remove 'context' command from test
|
2015-04-21 19:52:01 -07:00 |
|
Leonardo de Moura
|
fe9f4dd95f
|
fix(frontends/lean): another bug in sections with parameters
|
2015-04-21 19:50:21 -07:00 |
|
Leonardo de Moura
|
3df99e514b
|
fix(frontends/lean): problems with sections
|
2015-04-21 19:46:57 -07:00 |
|
Leonardo de Moura
|
9fb7aa9f1c
|
chore(tests): remove most occurrences of 'context' command from the test suite
|
2015-04-21 19:33:21 -07:00 |
|
Leonardo de Moura
|
76bf8de91a
|
refactor(hott): remove most 'context' commands from the HoTT library
|
2015-04-21 19:17:59 -07:00 |
|
Leonardo de Moura
|
670eac9d50
|
refactor(library): avoid 'context' command in the standard library
|
2015-04-21 19:13:19 -07:00 |
|
Leonardo de Moura
|
ce153d01f9
|
test(tests/lean/sec_notation2): notation nested in namespace/section/section
|
2015-04-21 19:07:52 -07:00 |
|
Leonardo de Moura
|
52e9ad1a98
|
feat(frontends/lean): allow persistent notation declaration in sections (when they do not contain parameters)
see issue #554
|
2015-04-21 19:04:06 -07:00 |
|
Leonardo de Moura
|
bf8a7eb9b4
|
fix(library/scoped_ext): bug in local metadata in sections
The problem is described in issue #554
|
2015-04-21 18:56:28 -07:00 |
|
Leonardo de Moura
|
697a536d9e
|
fix(library/tactic/inversion_tactic): type incorrect term being built by 'cases' tactic
fixes #545
|
2015-04-20 19:24:52 -07:00 |
|
Leonardo de Moura
|
68d4978953
|
feat(shell/lean): trap 'std::bad_alloc' and print nicer error message
See #489
|
2015-04-20 17:55:00 -07:00 |
|
Leonardo de Moura
|
47e37a3353
|
feat(kernel/metavar): add additional assertions
|
2015-04-20 17:46:06 -07:00 |
|
Leonardo de Moura
|
eb23a30626
|
feat(library/unifier): additional memory checks
|
2015-04-20 17:41:08 -07:00 |
|
Leonardo de Moura
|
28dad944c5
|
fix(library/unifier): cyclic assignment (?M <- ?M)
This was producing nonterminating behavior on example described at issue #489
|
2015-04-20 17:35:37 -07:00 |
|
Leonardo de Moura
|
431eade894
|
fix(library/tactic/inversion_tactic): incorrect use of optimization
|
2015-04-20 16:21:44 -07:00 |
|
Leonardo de Moura
|
107763a506
|
fix(frontends/lean): better error message for 'proof ... qed' blocks containing unsolved placeholders
|
2015-04-20 15:50:37 -07:00 |
|