Sebastian Ullrich
9ed678d80a
feat(frontends/lean/elaborator): structure notation: synthesize instance-implicit fields
2017-09-05 23:14:34 +02:00
Sebastian Ullrich
3aa5ebb8bd
feat(frontends/lean/elaborator): structure notation: allow explicit ctor param when given expected type
2017-09-05 23:14:34 +02:00
Sebastian Ullrich
da785d96a0
fix(frontends/lean/elaborator): synthesize metavars in e before trying to synthesize reflected e
2017-09-05 23:14:34 +02:00
Sebastian Ullrich
f255513fdc
fix(frontends/lean/definition_cmds): apply attributes after declaring equational lemmas
...
Fixes `@[simp] def ...`
2017-09-01 13:36:53 +02:00
Gabriel Ebner
05178ad950
chore(frontends/lean/decl_cmds,emacs/lean-syntax): typo
2017-08-28 17:04:03 +02:00
Leonardo de Moura
ac0be0ecc6
chore(frontends/lean/elaborator): style
2017-08-22 15:41:12 -07:00
Sebastian Ullrich
9e53147e0a
feat(frontends/lean/elaborator): allow field notation for recursive calls
2017-08-22 15:33:37 -07:00
Leonardo de Moura
971ae34521
feat(frontends/lean/elaborator): closes #1760
...
As described at issue #1760 , the new error message is:
```
1760.lean:6:18: error: type mismatch at application
f x
term
x
has type
big_type : Type 1
but is expected to have type
?m_1 : Type
```
2017-08-21 16:15:03 -07:00
Leonardo de Moura
049d940167
chore(frontends/lean/elaborator): cleanup
2017-08-18 17:50:29 -07:00
Leonardo de Moura
c149286f44
fix(frontends/lean/elaborator): add instantiate_pattern_mvars
2017-08-18 16:49:45 -07:00
Leonardo de Moura
d4f2bb77b8
feat(frontends/lean): recursive equation preprocessor
...
To make the equation compiler more convenient to use, we will add a
couple of preprocessing steps.
This commit adds the first one of them. In this step, we use
type inference to refine pattern variables, and we relax the
restrictions on inaccessible annotations.
We will also add a preprocessing step that implements the "complete
transition" step before we execute the elim_match step.
2017-08-18 15:06:11 -07:00
Gabriel Ebner
effd624911
fix(frontends/lean/parser): add check_system call
2017-08-18 08:54:04 +02:00
Leonardo de Moura
9927f331f4
chore(frontends/lean/elaborator): remove dead code
2017-08-17 16:03:32 -07:00
Leonardo de Moura
6315136279
fix(frontends/lean/definition_cmds): fixes #1790
2017-08-16 15:57:55 -07:00
Gabriel Ebner
867bc46d99
feat(library/vm/vm_parser): expose parse_command_like to the vm
2017-08-14 11:41:48 +02:00
Gabriel Ebner
fe5cb0106c
fix(frontends/lean/structure_cmd): disable def-eq check of pre-expressions
2017-08-02 14:41:35 +01:00
Gabriel Ebner
c500f9497d
feat(frontends/lean/structure_cmd): inherit default values in old_structure_cmd
2017-08-02 14:41:35 +01:00
Gabriel Ebner
becec82311
fix(frontends/lean/structure_cmd): simplify parser
2017-08-02 11:27:13 +01:00
Gabriel Ebner
b6f81e30e5
fix(frontends/lean/structure_cmd): prevent segfault
...
Fixes #1727 .
2017-08-02 11:27:13 +01:00
Gabriel Ebner
403234f29e
fix(frontends/lean/interactive): fix empty prefix in autocompletion
2017-08-01 18:42:31 +01:00
Gabriel Ebner
6d0a7a80af
fix(frontends/lean/builtin_exprs): prevent segfault
2017-08-01 14:57:37 +01:00
Gabriel Ebner
c15f2979c6
fix(frontends/lean/util): allow docstrings after variables
2017-08-01 10:18:05 +01:00
Gabriel Ebner
2804a0ea27
fix(util/name): escape empty name components using french quotes
2017-07-31 16:01:46 +01:00
Sebastian Ullrich
c44ed73d56
fix(frontends/lean/scanner): minor lexical grammar fixup
2017-07-26 17:02:00 +02:00
Leonardo de Moura
4faae27069
perf(frontends/lean): add notation #[...]
...
The new notation should be use to input long sequences.
Closes #1755
2017-07-21 04:20:48 -07:00
Sebastian Ullrich
7e619487f0
fix(frontends/lean/elaborator): suppress error messages containing synthetic sorrys
2017-07-21 01:46:31 -07:00
Sebastian Ullrich
46c1a1a844
refactor(frontends/lean/elaborator,kernel/error_msgs): remove duplicate code
2017-07-21 01:46:31 -07:00
Sebastian Ullrich
f8cfc4ea1b
feat(kernel/error_msgs,frontends/lean/elaborator): add more context to 'type/function expected' errors
2017-07-21 01:46:31 -07:00
Sebastian Ullrich
ae5bc52d97
fix(frontends/lean/elaborator): pass expected type through visit_function
2017-07-20 01:58:29 -07:00
Sebastian Ullrich
9e8d30ec74
fix(frontends/lean/elaborator): suppress errors in visit_overloaded
2017-07-20 01:58:29 -07:00
Sebastian Ullrich
9ed72acabe
fix(frontends/lean/builtin_exprs): allow constant patterns in do notation
2017-07-20 01:51:00 -07:00
Sebastian Ullrich
9c2d42b269
fix(frontends/lean/parser): to_pattern_fn: replace invalid choice pattern with sorry
...
Fixes #1749
2017-07-17 14:59:07 +02:00
Leonardo de Moura
9afb53fad5
feat(kernel/expr): allow metavariables to have user-facing names
...
We need this feature for:
1) Defining nonlinear search patterns. Example: (?m <= ?m + 1)
2) Preprocessing recursive equations and support the pattern
refinement approach used in Agda. Example: in Agda, they accept
```
def append {A : Type} : Π (m n : nat), Vec A m -> Vec A n -> Vec A (m + n)
| m n nil ys := ys
| m n (cons m' x xs) ys := cons x (append m' n xs ys)
```
These equations have to be refined. For example, `m` has to be
replaced with `0` (in the first equation), and `succ m'` in the
second. To implement this kind of refinement, we need to convert
the pattern variables (local constants) into metavariables during
elaboration. Then, the unassigned metavariables become local constants
again. This preprocessing step will fix some of the issues on #1594 .
To completely fix #1594 , we will need yet another preprocessing step
which will implement "complete transition" used in the equation
compiler before we start elim_match.cpp
2017-07-16 07:16:41 -07:00
Gabriel Ebner
246d71f3ff
feat(library/equations_compiler): error recovery
2017-07-16 05:17:38 -07:00
Gabriel Ebner
9367e94900
fix(frontends/lean/pp): hide proof terms in non-proofs by default
...
This is mainly to reduce clutter. Proof term printing can still be
forced using the `pp.proofs` option.
2017-07-15 22:21:22 +01:00
Gabriel Ebner
37d9e03cc1
feat(frontends/lean/pp): show substituted expressions for delayed abstractions
...
@leodemoura I tried to look up the unique names in the local context,
but this pretty much always fails. AFAICT we never remember the local
context when pretty-printing expression texts.
2017-07-15 21:34:05 +01:00
Gabriel Ebner
68ee9396c6
fix(frontends/lean/parser): support backtracking from empty expressions
...
Fixes #1745 .
2017-07-15 11:12:09 +01:00
Gabriel Ebner
3392aa90b5
fix(frontends/lean/definition_cmds): support parameters in mutual defs
2017-07-13 15:14:46 +01:00
Leonardo de Moura
8dcccd3bfc
fix(frontends/lean/parser): make sure imax and max level arguments are parsed using the same precendence we use to parse application arguments
...
This commit addresses an issue raised by @digama0 on the Lean slack channel.
2017-07-07 12:43:07 -07:00
Gabriel Ebner
d610709a53
fix(frontends/lean/print_cmd): report error on unknown identifier
2017-07-06 19:58:30 +02:00
Leonardo de Moura
1bfaf19277
chore(library/delayed_abstraction): clarify delayed_abstraction API
2017-07-05 16:40:45 -07:00
Sebastian Ullrich
8ac1ea6b18
feat(frontends/lean/tactic_notation): ignore by keyword in interactive tactic mode
2017-07-05 11:20:10 -07:00
Sebastian Ullrich
c8d6b40991
refactor(frontends/lean/builtin_exprs,library): suppose ~> assume :
2017-07-05 11:20:10 -07:00
Sebastian Ullrich
f024ccd75d
refactor(frontends/lean/token_table,library): take ~> assume
2017-07-05 11:20:10 -07:00
Sebastian Ullrich
f95f70fe56
feat(frontends/lean/builtin_exprs): support have ... := ... in term mode
2017-07-05 11:20:10 -07:00
Sebastian Ullrich
2f73a38637
refactor(frontends/lean/builtin_exprs): simplify parse_have
2017-07-05 11:20:10 -07:00
Sebastian Ullrich
2ca44459ba
feat(init/meta/interactive): add from synonym for exact
2017-07-05 11:20:10 -07:00
Sebastian Ullrich
2b35a9b1f0
fix(frontends/lean/notation_cmd): notation: default binding power for leading tokens to max
2017-07-05 17:30:38 +02:00
Sebastian Ullrich
ad97607307
fix(frontends/lean/tactic_notation): always use quote_scope for parsing interactive parameters
...
Replace now redundant `qexpr` parser with `parser.pexpr`
2017-07-04 12:20:38 -07:00
Leonardo de Moura
95c7c697a6
refactor(library/tactic/simp_lemmas): simp set generation should not be affected by transparency setting
2017-07-01 12:54:37 -07:00
