Gabriel Ebner
eea61a1991
fix(frontends/lean/definition_cmds): fix trace messages in proofs
2017-05-23 11:14:31 -07:00
Gabriel Ebner
d4b45abad6
fix(frontends/lean/elaborator): ground universe meta-variables in tactic terms
2017-05-23 11:14:30 -07:00
Gabriel Ebner
dd91ef3b22
fix(frontends/lean/elaborator): fix compilation with gcc
2017-05-23 11:14:30 -07:00
Gabriel Ebner
6b956ad658
fix(frontends/lean): prevent endless loops
2017-05-23 11:14:30 -07:00
Gabriel Ebner
33c737fc53
feat(frontends/lean/brackets): allow trailing commas in brackets
2017-05-23 11:14:30 -07:00
Gabriel Ebner
345cd1bc2a
feat(frontends/lean/parser): error recovery in interactive tactics
2017-05-23 11:14:30 -07:00
Gabriel Ebner
0b133f1f2a
feat(frontends/lean/elaborator): error recovery for structure instances
2017-05-23 11:14:30 -07:00
Gabriel Ebner
8c80cb8fe9
feat(frontends/lean/equations_validator): report errors instead of
...
exceptions
2017-05-23 11:14:30 -07:00
Gabriel Ebner
00ac867ddf
feat(frontends/lean/elaborator,library/sorry): suppress error message that mention synthetic sorrys
2017-05-23 11:14:30 -07:00
Gabriel Ebner
1468461c47
feat(frontends/lean): recover from many parser errors
2017-05-23 11:14:30 -07:00
Sebastian Ullrich
5a19430f60
fix(frontends/lean/scanner): wrong upos after field projection
2017-05-23 10:33:31 +02:00
Gabriel Ebner
54114fd7bd
fix(frontends/lean/tactic_notation): do not clamp errors to the end of {} blocks
2017-05-23 07:28:34 +02:00
Leonardo de Moura
729e798d6f
feat(frontends/lean/definition_cmds): copy equational lemmas to top level definition
2017-05-22 14:51:06 -07:00
Gabriel Ebner
07c25338b9
feat(shell/server): add search command
2017-05-22 09:40:38 -07:00
Leonardo de Moura
9fb7e5c931
feat(library/equations_compiler): generate equational lemmas for auxiliary _main definitions
2017-05-21 15:21:28 -07:00
Leonardo de Moura
ce71b4c5c2
feat(frontends/lean/definition_cmds): define top-level mutual definitions
...
We still need the equational lemmas.
2017-05-21 10:26:43 -07:00
Leonardo de Moura
4e496b78d5
feat(library/equations_compiler): unpack auxiliary definition
...
We still need to unpack auxiliary lemmas, and propagate information in
the frontend.
2017-05-20 20:34:18 -07:00
Leonardo de Moura
789d4e148f
feat(library/equations_compiler): add pack_mutual
...
This step packs a collection of mutually recursive functions into a
single one. We use `psum` to combine the different domains, and
`psum.cases_on` to combine the codomains.
2017-05-18 15:29:51 -07:00
Leonardo de Moura
2f301d5fc7
fix(frontends/lean/pp): fix previous commit
2017-05-18 14:24:19 -07:00
Leonardo de Moura
323060df26
fix(frontends/lean/pp): pp for mutual definitions
...
missing line break
2017-05-18 11:46:14 -07:00
Leonardo de Moura
cf9a5128c1
fix(frontends/lean/definition_cmds): check_valid_end_of_equations
...
'with' token was missing.
2017-05-18 11:28:02 -07:00
Sebastian Ullrich
9b86808345
fix(frontends/lean/structure_cmd): parent structures may use different universe params
...
Fixes #1585
2017-05-18 09:35:14 -07:00
Sebastian Ullrich
9fdf11fa54
fix(frontends/lean/pp): shadowing shortened const
...
Fixes #1584
2017-05-18 09:35:14 -07:00
Sebastian Ullrich
75786e9a6e
feat(frontends/lean/pp): hide (some) defaulted arguments on pp.implicit true
2017-05-17 10:38:12 -07:00
Sebastian Ullrich
84997bf4de
refactor(init/meta/expr): unify expr and pexpr
2017-05-17 10:38:12 -07:00
Sebastian Ullrich
aefd312a98
feat(frontends/lean/decl_util): allow opt_param shorthand in all decls
2017-05-17 10:38:12 -07:00
Sebastian Ullrich
5f3e0a1cc4
feat(frontends/lean/decl_cmds): allow implicit locals in constants & axioms
2017-05-17 10:38:12 -07:00
Leonardo de Moura
4575c9e038
feat(frontends/lean): swap (t) and ``(t) semantics
2017-05-15 09:41:31 -07:00
Sebastian Ullrich
14425bd2d3
fix(frontends/lean/decl_util): double-elaboration of include params
2017-05-14 19:19:22 -07:00
Sebastian Ullrich
818c041922
fix(frontends/lean/scanner): skip_to_pos was skipping bytes instead of chars
2017-05-14 19:19:22 -07:00
Sebastian Ullrich
42eb0c680e
feat(kernel/inductive,library/inductive_compiler): do not enforce positivity rule on meta inductives
2017-05-14 19:17:28 -07:00
Gabriel Ebner
85673cdd8d
fix(frontends/lean/definition_cmds): examples in noncomputable theories
2017-05-13 09:04:07 +02:00
Sebastian Ullrich
ead6318ee0
feat(frontends/lean/elaborator): substitute reflected locals into expr quotes
2017-05-09 16:02:41 -07:00
Sebastian Ullrich
8c0394b294
refactor(library,frontends/lean): separate expr and pexpr macros
2017-05-09 16:02:41 -07:00
Sebastian Ullrich
2825c5fbcc
feat(frontends/lean/elaborator): elaborate ``(e) to type reflected e` if possible and add coercion reflected -> expr
2017-05-09 16:02:41 -07:00
Gabriel Ebner
d2b6b3f573
fix(frontends/lean/elaborator): fix segfault
2017-05-09 18:06:25 +02:00
Sebastian Ullrich
3c525bef6a
fix(frontends/lean/pp): parenthesize Type u where necessary
2017-05-03 13:27:35 -07:00
Sebastian Ullrich
7eb04f0d44
fix(frontends/lean/elaborator): instantiate mvars in [reflected a] params
...
Fixes #1562
2017-05-03 13:27:35 -07:00
Sebastian Ullrich
b37b1fb7c6
refactor(library/type_context,frontends/lean/elaborator): move reflected code back into elaborator
...
Since we do not want recursive special handling of `reflected`, this seems to be
the simpler design.
2017-05-03 13:27:35 -07:00
Leonardo de Moura
a0a8103804
chore(frontends/lean): go back to 'c' as notation for characters
...
This suggestion has been discussed at Slack.
We have decided to use #"c" as notation because we wanted to allow `'`
in the beginning of identifiers like in SML and F*. In particular,
we wanted to allow users to use 'a 'b 'c for naming type parameters
like in SML. However, nobody used this notation. In the Lean standard
library, we are using greek letters for naming type parameters.
So, there is no real motivation for the ugly #"c" syntax.
2017-05-02 13:00:51 -07:00
Leonardo de Moura
f64b3cb874
chore(frontends/lean): do not allow identifiers starting with '
2017-05-02 10:43:44 -07:00
Sebastian Ullrich
1102234932
fix(frontends/lean/elaborator): guard against unexpected sorry macro
...
Fixes #1559
2017-05-02 13:57:16 +02:00
Sebastian Ullrich
07b1cfb268
fix(frontends/lean/structure_cmd): do not combine field default overrides and parent field short-hands
...
Fixes #1557
2017-05-02 13:42:15 +02:00
Leonardo de Moura
55fee26b36
feat(library/class): add attribute for tracking symbols occurring in instances of type classes
...
For more information see:
https://github.com/leanprover/lean/wiki/Refactoring-structures
The new attribute [algebra] implements the [algebraic_class] described
in the page above.
2017-05-01 18:02:30 -07:00
Daniel Selsam
8b8814cfbe
fix(frontends/lean/inductive_cmd.cpp): fixes #1525
2017-05-01 14:57:25 -07:00
Gabriel Ebner
3810e8950d
refactor(util/lean_path,util/path): separate search path functions
2017-05-01 14:11:38 -07:00
Gabriel Ebner
d79909a1b8
refactor(util/lean_path): support leanpkg.path files
2017-05-01 14:11:38 -07:00
Gabriel Ebner
baa4c48f1f
refactor(util/lean_path): explicitly pass around search path
2017-05-01 14:11:38 -07:00
Leonardo de Moura
ba5eccdca8
refactor(library/init/core): rename out_param => inout_param
...
It is really input/output.
2017-05-01 14:01:41 -07:00
Leonardo de Moura
66a1fec94e
feat(library/init/category): add has_orelse type class
2017-05-01 09:58:27 -07:00
