Leonardo de Moura
d41e055d1c
feat(frontends/lean/migrate_cmd): catch memory error in the migrate command
2015-04-27 12:58:11 -07:00
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
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
8241863abe
feat(kernel/hits): add two builtin HITs: type_quotient and trunc
2015-04-23 15:32:31 -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
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
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
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
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
Leonardo de Moura
df05edf333
feat(frontends/lean): generate warning when 'exit' is used
...
closes #553
2015-04-20 14:45:39 -07:00
Leonardo de Moura
6f6d106a10
feat(library/tactic): add "check_expr" tactic
...
closes #486
2015-04-19 19:00:05 -07:00
Leonardo de Moura
60e320fd79
feat(frontends/lean): protected constants and axioms
...
fixes #527
2015-04-19 17:45:58 -07:00
Leonardo de Moura
b7ca2a0ec9
fix(library/tactic/exact_tactic): exact and or_else
...
fixes #543
2015-04-19 17:23:09 -07:00
Soonho Kong
3d79f89f5e
fix(emacs/lean-mode): lean-execute
...
shell-quote-argument also escapes '~' into '\~' which causes a problem.
This fix first calls 'f-full' to get a absolute path, then call
shell-quote-argument.
close #544
2015-04-16 19:27:42 -04:00
Soonho Kong
20b594e1cd
fix(emacs/lean-mode.el): use 'shell-quote-argument' in lean-execute
...
close #544
2015-04-13 14:19:39 +01:00
Leonardo de Moura
5d95cb0979
feat(library/tactic): add 'refine' tactic
...
closes #482
2015-04-06 18:36:56 -07:00
Leonardo de Moura
412f03b08b
feat(library/tactic/exact_tactic): generate error if 'exact' tactic produces a term containing metavariables
2015-04-06 13:38:53 -07:00
Leonardo de Moura
2bc13f6bfd
feat(library/tactic/exact): enforce goal type during elaboration when executing 'exact' tactic
...
Remark: this was the behavior of the 'sexact' tactic.
This commit also adds the 'rexact' (relaxed exact) tactic which does not
enforce the goal type.
closes #495
2015-04-06 13:23:38 -07:00
Leonardo de Moura
754276a660
feat(frontends/lean): round parenthesis for [tactic1 | tactic2]
...
This commit also replaces the notation for divides
`(` a `|` b `)`
with
a `∣` b
The character `∣` is entered by typing \|
closes #516
2015-04-06 09:24:09 -07:00
Leonardo de Moura
969d17fd12
fix(frontends/lean/elaborator): class inference in tactic mode with trunc
...
closes #477
2015-04-05 17:47:14 -07:00
Leonardo de Moura
d731a4ab13
feat(library/normalize): add '[unfold-f]' hint
...
closes #497
2015-04-05 03:00:13 -07:00
Leonardo de Moura
d591c63840
feat(frontends/lean/decl_cmds): allow local coercions in contexts
...
closes #525
2015-04-04 15:25:07 -07:00
Leonardo de Moura
8c59f17605
feat(frontends/lean): 'using' expression without 'show' or 'have'
...
closes #536
2015-04-04 15:25:07 -07:00
Leonardo de Moura
4ec0e1b07c
feat(frontends/lean): improve calc mode
...
Now, it automatically supports transitivity of the form
(R a b) -> (b = c) -> R a c
(a = b) -> (R b c) -> R a c
closes #507
2015-04-04 08:58:35 -07:00
Leonardo de Moura
1150b19598
perf(frontends/lean/elaborator): do not invoke recursive equation compiler when equations still contain metavariables
2015-04-02 23:37:33 -07:00
Soonho Kong
1f20fb6e9e
feat(emacs/lean-input): add not(¬) and iff(↔)
...
close leanprover/tutorial#81
2015-04-02 22:13:01 -04:00