Leonardo de Moura
fee2b002fc
fix(util/exception): typo in error message
2015-04-27 12:02:04 -07:00
Leonardo de Moura
dcc94dde82
refactor(kernel): rename may_reduce_later to is_stuck, and make is_stuck more precise
...
It now reflects the definition used in the elaboration paper.
2015-04-27 11:20:15 -07:00
Leonardo de Moura
68383d49de
refactor(shell/lean): remove useless output
...
It was added for implementing the web version, and avoid the need to
simulate a file system in the web browser.
It turns out we decided to use a virtual file system.
2015-04-27 10:15:01 -07:00
Leonardo de Moura
76c773ad3d
feat(library/data/examples/depchoice): add dependent choice example
2015-04-26 12:56:23 -07:00
Leonardo de Moura
072bf0b3b4
refactor(library): make sure "choose" compute inside the kernel
2015-04-25 23:10:48 -07:00
Leonardo de Moura
d455bb4c5b
feat(library/data/fintype): add decidable_exists_finite
2015-04-25 21:38:03 -07:00
Leonardo de Moura
6bb6644c25
feat(library/data/squash): define squash type using quotients
2015-04-24 18:11:25 -07:00
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
