Leonardo de Moura
|
8e6de93394
|
fix(frontends/lean/parser): add two kinds of no_undef_id behavior: to (global) constant; to local constant
|
2014-10-26 09:47:11 -07:00 |
|
Leonardo de Moura
|
212ae0b61c
|
feat(frontends/lean): automatically add 'info' tactic in begin-end blocks
Actually, the tactic is only added when Lean is in collect-info mode.
|
2014-10-23 13:30:04 -07:00 |
|
Leonardo de Moura
|
38a9aa2a98
|
feat(frontends/lean): automatically open 'tactic' namespace (if it is not already open) in 'by' and 'begin-end' expressions
|
2014-10-23 10:26:19 -07:00 |
|
Leonardo de Moura
|
eb2b59ce4f
|
refactor(frontends/lean): remove unnecessary files
|
2014-10-22 17:33:16 -07:00 |
|
Leonardo de Moura
|
5e15ac0c92
|
feat(library/tactic): add new approach for embedding non-elaborated expressions into tactics
|
2014-10-22 17:29:50 -07:00 |
|
Leonardo de Moura
|
7c617955d0
|
refactor(library/tactic): move 'exact' tactic to separate module
|
2014-10-22 17:29:44 -07:00 |
|
Leonardo de Moura
|
9b8f60b739
|
feat(frontends/lean/builtin_exprs): tolerate dangling ',' in begin-end block
This is useful when debugging proofs.
|
2014-10-20 15:59:49 -07:00 |
|
Leonardo de Moura
|
a3aca96cb9
|
fix(frontends/lean/builtin_exprs): error position
|
2014-10-20 15:56:58 -07:00 |
|
Leonardo de Moura
|
fd40999909
|
feat(frontends/lean): uniform unsolved goals "error" position
|
2014-10-20 15:52:06 -07:00 |
|
Leonardo de Moura
|
3b6b23c921
|
refactor(kernel/expr): remove silly overloads
|
2014-10-16 13:37:55 -07:00 |
|
Leonardo de Moura
|
28128e0330
|
fix(frontends/lean): EXTRA_TYPE info
|
2014-10-16 12:25:18 -07:00 |
|
Leonardo de Moura
|
58c9421bab
|
refactor(library/tactic): elaborate expressions nested in tactics with respect to current goal, save postponed constraints (e.g., flex-flex constraints) closes #44, fixes #70
|
2014-10-14 17:18:40 -07:00 |
|
Leonardo de Moura
|
c0725d1934
|
refactor(frontends/lean): remove 'including' expressions
|
2014-10-03 09:09:27 -07:00 |
|
Leonardo de Moura
|
f78d831de3
|
refactor(frontends/lean): remove hardcoded Type', and define it using notation
|
2014-10-02 14:29:51 -07:00 |
|
Leonardo de Moura
|
ead827d6b7
|
feat(frontends/lean): add ! operator the "dual" of @ , closes #220
|
2014-10-01 17:13:41 -07:00 |
|
Leonardo de Moura
|
29d6bff785
|
refactor(frontends/lean): explicit initialization/finalization
|
2014-09-23 10:00:36 -07:00 |
|
Leonardo de Moura
|
010ecebfea
|
feat(frontends/lean): add proof-qed expression
Remark: we still have to add support to it in the elaborator.
Right now, it is just an embellished parenthesis.
|
2014-09-11 18:14:49 -07:00 |
|
Leonardo de Moura
|
7ffe73b8ca
|
fix(frontends/lean): name clash inside section, fixes #181
|
2014-09-11 16:37:23 -07:00 |
|
Leonardo de Moura
|
b4793df653
|
feat(frontends/lean): rename '[fact]' to '[visible]'
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
|
2014-09-08 07:47:42 -07:00 |
|
Leonardo de Moura
|
3310eb3dfc
|
feat(frontends/lean): remove restriction on implict arguments, add new test that demonstrates the new feature
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
|
2014-09-07 12:29:32 -07:00 |
|
Leonardo de Moura
|
de8a71bc5b
|
perf(frontends/lean): do not create extra_info annotation when we are not collecting info
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
|
2014-09-04 11:25:41 -07:00 |
|
Leonardo de Moura
|
b94ec07b29
|
feat(frontends/lean): associate type information with left '('
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
|
2014-09-04 09:56:27 -07:00 |
|
Leonardo de Moura
|
5a203d1c75
|
feat(frontends/lean): add '?' for inspecting the type of any expression, it produces a EXTRA_TYPE info entry
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
|
2014-09-03 11:54:42 -07:00 |
|
Leonardo de Moura
|
b9489ce585
|
fix(frontends/let): let-expression pretty printer
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
|
2014-08-29 10:58:27 -07:00 |
|
Leonardo de Moura
|
be56fcf0bd
|
fix(frontends/lean/pp): pretty print 'let-expressions', closes #87
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
|
2014-08-28 18:20:58 -07:00 |
|
Leonardo de Moura
|
1e80a9dfe9
|
feat(frontends/lean): avoid exponential blowup when processing let-expressions with a lot of sharing, cleanup show-expression
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
|
2014-08-28 16:27:52 -07:00 |
|
Leonardo de Moura
|
8719dff361
|
fix(frontends/lean): distribute '@' over choice
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
|
2014-08-27 16:31:18 -07:00 |
|
Leonardo de Moura
|
01000ff7df
|
feat(library): add typed_expr macro
We use it to enforce that a let-variable has the expected type
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
|
2014-08-22 11:26:06 -07:00 |
|
Leonardo de Moura
|
d4ac482d76
|
refactor(kernel): move annotation to library
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
|
2014-08-22 10:38:10 -07:00 |
|
Leonardo de Moura
|
07bc0727e2
|
feat(frontends/lean): 'let [inline]' is the default
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
|
2014-08-21 18:24:22 -07:00 |
|
Leonardo de Moura
|
725f5ba0a0
|
feat(frontends/lean): use 'begin-end' instead of 'proof-qed' for blocks of tactics, closes #81
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
|
2014-08-21 16:58:25 -07:00 |
|
Leonardo de Moura
|
6a6c9f472e
|
feat(frontends/lean): add synthesis information only for 'explicit' placeholder
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
|
2014-08-15 12:48:36 -07:00 |
|
Leonardo de Moura
|
2869d9059f
|
feat(frontends/lean): change 'proof-qed' semantics: no backtracking
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
|
2014-08-12 17:40:30 -07:00 |
|
Leonardo de Moura
|
6ca80b5000
|
feat(frontends/lean): add 'sorry'
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
|
2014-07-31 18:35:57 -07:00 |
|
Leonardo de Moura
|
0cdd4a267c
|
feat(frontends/lean/pp): pretty print 'show' expressions
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
|
2014-07-26 21:56:35 -07:00 |
|
Leonardo de Moura
|
60cc9ac8e2
|
feat(frontends/lean/pp): pretty print 'have' expressions
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
|
2014-07-26 21:35:26 -07:00 |
|
Leonardo de Moura
|
cf35c07786
|
fix(frontends/lean): fix 'let' annotation placement and pretty printer
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
|
2014-07-26 21:00:22 -07:00 |
|
Leonardo de Moura
|
a59eec39b8
|
feat(frontends/lean): improve 'type mismatch' error position, and annotate 'have'-expressions
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
|
2014-07-25 09:44:40 -07:00 |
|
Leonardo de Moura
|
022a151cf7
|
feat(kernel): add general purpose 'annotations', they are just a generalization of the 'let'-annotations
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
|
2014-07-25 09:33:31 -07:00 |
|
Leonardo de Moura
|
5eaf04518b
|
refactor(*): rename Bool to Prop
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
|
2014-07-22 09:43:18 -07:00 |
|
Leonardo de Moura
|
2e6184a721
|
fix(frontends/lean): more bugs in section management
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
|
2014-07-14 06:27:36 +01:00 |
|
Leonardo de Moura
|
b53e6eda58
|
refactor(frontends/lean): eliminate the abstract method 'family' from parser
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
|
2014-07-14 05:44:06 +01:00 |
|
Leonardo de Moura
|
1d273fcfdd
|
chore(frontends/lean): rename 'obtains' to 'obtain'
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
|
2014-07-12 06:35:24 +01:00 |
|
Leonardo de Moura
|
024299f56b
|
fix(frontends/lean): name of auxiliary hypothesis in 'obtains' expression, and also marked them as non-contextual
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
|
2014-07-11 04:50:53 +01:00 |
|
Leonardo de Moura
|
cf34f75ab5
|
feat(frontends/lean): add 'obtains' expression
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
|
2014-07-11 04:08:51 +01:00 |
|
Leonardo de Moura
|
313c7066e7
|
feat(frontends/lean): add Type' as notation for Type.{_+1}
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
|
2014-07-10 13:28:36 +01:00 |
|
Leonardo de Moura
|
b43fb7448c
|
feat(frontends/lean): search for identifiers in the stack of namespaces; reject non-atomic names as local names
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
|
2014-07-07 19:00:06 -07:00 |
|
Leonardo de Moura
|
6ea7bb3ea4
|
feat(frontends/lean/builtin_exprs): add 'including' expression
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
|
2014-07-04 18:37:09 -07:00 |
|
Leonardo de Moura
|
e3ab0a1d10
|
feat(frontends/lean): improve error messages when users forget to import 'tactic'
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
|
2014-07-03 08:33:29 -07:00 |
|
Leonardo de Moura
|
a7d660f875
|
feat(frontends/lean): add command for customizing the behavior of proof-qed blocks: we can automatically register tactics to be automatically applied before each component
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
|
2014-07-02 20:45:10 -07:00 |
|