Leonardo de Moura
3c1ccc9b74
refactor(kernel): use m_meta instead of m_trusted
2018-05-31 11:18:00 -07:00
Leonardo de Moura
75c63ec921
refactor(*): list<name> ==> obj_list<name>
2018-05-23 15:48:43 -07:00
Leonardo de Moura
4af1f31877
feat(util, kernel): add obj_list wrapper for Lean list objects, and use it to implement list of universe levels
2018-05-23 14:48:22 -07:00
Leonardo de Moura
0556412f8d
refactor(*): add runtime folder
...
@kha The runtime folder includes what is needed to link a
standalone Lean program. It is still contains some unnecessary files.
We will be able to remove them after we release Lean4.
2018-05-14 14:23:56 -07:00
Leonardo de Moura
bdea7d420d
chore(*): type_context ==> type_context_old
2018-03-05 12:38:24 -08:00
Sebastian Ullrich
1abf8738fc
feat(frontends/lean/structure_cmd): allow implicitness infer annotation and parameters in field declaration
2018-02-28 12:49:22 +01:00
Leonardo de Moura
28d6326228
refactor(frontends/lean/parser): add name_generator
2018-02-21 15:04:19 -08:00
Sebastian Ullrich
86e231e6c9
feat(frontends/lean/structure_cmd): make superclass fields inst implicit
2018-02-02 08:58:53 -08:00
Sebastian Ullrich
040748419f
refactor(frontends/lean/elaborator): refactor and document structure instance notation code
2018-02-02 08:58:53 -08:00
Leonardo de Moura
9eb22cd548
feat(library/constructions/injective): automatically generate auxiliary lemma *.inj_eq for constructors
...
We are going to use these lemmas in the simplifier.
2018-01-12 16:41:12 -08:00
Leonardo de Moura
7d3133a845
fix(frontends/lean/structure_cmd): do not generate equation lemma for _default meta definitions
2017-11-22 12:24:51 -08:00
Sebastian Ullrich
d037ab1d4b
refactor(frontends/lean/structure_cmd): remove awkward pointer index computation
2017-11-17 16:31:30 -08:00
Sebastian Ullrich
aa8791a9ee
fix(frontends/lean/structure_cmd): support dependent parents in new structure cmd
2017-11-17 16:31:30 -08:00
Sebastian Ullrich
716c730c38
fix(frontends/lean/structure_cmd): allow extending structures in the current context
2017-10-23 11:12:14 -07:00
Sebastian Ullrich
2faad5114a
chore(frontends/lean): enforce and document applying attributes last
2017-09-14 18:48:18 +02:00
Gabriel Ebner
341cf71fb9
fix(frontends/lean/structure_cmd): check parent expression after elaboration as well
2017-09-14 09:36:40 +02:00
Sebastian Ullrich
7412512579
fix(frontends/lean/structure_cmd): apply attributes last
2017-09-11 16:56:02 -07:00
Leonardo de Moura
d428eca8a7
fix(library/equations_compiler,frontends/lean): private name support and alias generation for auxialiary declarations
...
fixes #1804
Remark: now, all auxiliary definitions in a private declaration share
the same "private" prefix.
2017-09-11 16:46:56 -07:00
Leonardo de Moura
51bac2918f
chore(library/init/core): declare and using structure
...
This change was requested by several users.
2017-09-05 15:08:20 -07: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
Leonardo de Moura
0b19ef82e1
feat(frontends/lean/structure_cmd): default parameter for structure/class declarations
...
Remark: we support them at inductive declarations.
2017-06-28 12:20:56 -07:00
Leonardo de Moura
c7e68e57cf
fix(frontends/lean/structure_cmd): fixes #1681
...
@kha I'm not sure if this is the right fix. I just avoided the loop that adds
`mk_expr_placeholder` if the function is not a projection.
I didn't spend time investigating why we need `mk_proj_app`.
I know the library doesn't compile if we don't use it, and just use
```
return mk_app(copy_tag(ref, mk_constant(S_name + fname)), e);
```
:)
2017-06-19 16:22:38 -07:00
Sebastian Ullrich
95b317fa64
refactor(frontends/lean): do not hard code commands accepting attributes & modifiers
2017-06-19 11:09:26 -07:00
Sebastian Ullrich
09987df06e
fix(frontends/lean/structure_cmd): do not collect m_ctx_locals multiple times
2017-06-01 07:38:30 -07:00
Sebastian Ullrich
1977b5bfc9
refactor(frontends/lean/structure_cmd): also simplify collecting ctx levels
2017-06-01 07:38:30 -07:00
Sebastian Ullrich
25152bc80d
fix(frontends/lean/structure_cmd): use collect_implicit_locals to catch more context locals
...
Fixes #1623
2017-06-01 07:38:30 -07:00
Sebastian Ullrich
4eab11ec3d
fix(frontends/lean/structure_cmd): even less error recovery
2017-05-30 19:02:25 +02:00
Gabriel Ebner
b14a248dcd
fix(frontends/lean/structure_cmd): segfault
2017-05-29 07:37:50 +02: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
42eb0c680e
feat(kernel/inductive,library/inductive_compiler): do not enforce positivity rule on meta inductives
2017-05-14 19:17:28 -07: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
Leonardo de Moura
5cef84709f
refactor(library): avoid auxiliary definitions such as add/mul/le/etc
...
See Section "Other goodies" at
https://github.com/leanprover/lean/wiki/Refactoring-structures
This commit also improves the support for projections in the
unifier/matcher.
Now, we consider the extra case-split for projections.
Given a projection `proj`, and the constraint `proj s =?= proj t`, we need to try first `s =?= t` and if it fails, then try to reduce.
This is needed in the standard library because we now have constraints such as:
```
@has_le.le ?A ?s ?a ?b =?= @has_le.le nat nat.has_add x y
```
If we reduce the right hand side, we get the unsolvable constraint
```
@has_le.le ?A ?s ?a ?b =?= nat.le x y
```
Before this change, the constraint was `@le ?A ?s ?a ?b =?= @le nat nat.has_add x y`, and we already perform a case-split in this case.
Moreover, projections were eagerly reduced whenever possible.
The extra case-split generates a performance problem in several tests. For example `fib 8 = 34` was timing out.
I worked around this issue by performing the case-split only when the constraint contains meta-variables.
There are also minor issues. Example. `<` is notation for `has_lt.lt`, but `>` is for `gt`.
2017-05-01 08:52:19 -07:00
Gabriel Ebner
ca2eab3a2f
fix(frontends/lean/structure_cmd): instantiate universe levels in projections to parents
2017-04-29 15:00:17 +02:00
Sebastian Ullrich
cfbc449769
refactor(frontends/lean/structure_cmd): some more cleanup
2017-04-26 14:22:46 -07:00
Sebastian Ullrich
d968b9a1c8
fix(frontends/lean/structure_cmd): remove evil Pi overload that accidentally abstracted constants in structure decls
2017-04-26 14:22:36 -07:00
Sebastian Ullrich
dd1f3e5f8c
fix(frontends/lean/structure_cmd): reject internal field names
...
Fixes #1539
2017-04-25 17:47:08 -07:00
Sebastian Ullrich
e9a6c544af
refactor(frontends/lean/{elaborator,structure_cmd}): compile structure inheritance to nested fields
2017-04-24 19:35:15 +02:00
Leonardo de Moura
9a4e04b8ca
feat(frontends/lean/structure_cmd): add equational lemma for auxiliary default values
2017-03-27 21:37:31 -07:00
Sebastian Ullrich
55425e7b1f
fix(frontends/lean/structure_cmd): unfold untrusted macros in intro rules
2017-03-27 13:42:08 -07:00
Sebastian Ullrich
bf8292cb17
feat(frontends/lean/structure_cmd): allow local notations
2017-03-27 13:42:08 -07:00
Leonardo de Moura
36770119b6
feat(library): do not generate C.destruct (for structures), and C.induction_on (for structures and inductive datatypes)
2017-03-15 14:45:13 -07:00
Daniel Selsam
7f56f23e70
chore(frontends/lean/inductive_cmds): allow sorrys
2017-03-15 14:06:56 -07:00
Daniel Selsam
538ac8d187
feat(inductive_compiler): generate injectivity lemmas
2017-03-10 22:27:18 -08:00
Leonardo de Moura
23935ee390
feat(frontends/lean): allow auto_param notation in structure declarations
...
See #1422
TODO: take the auto_param into account in the `{ ... }` notation.
2017-03-08 15:41:30 -08:00
Sebastian Ullrich
970e11bf5e
feat(frontends/lean/{elaborator,structure_cmd}): allow overriding field defaults
2017-03-08 10:41:20 -08:00
Daniel Selsam
5f0ebf90de
fix(frontends/lean/structure_cmd): call inductive compiler without params in type
2017-03-06 14:01:46 -08:00
