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
21e52408b2
refactor(library/constructions): make sure constructions do not use ::lean::mk_fresh_name
2018-02-21 15:04:19 -08:00
Sebastian Ullrich
dc5e50e7f0
feat(frontends/lean/structure_cmd): hide out_param in projections
2018-02-02 08:58:52 -08:00
Sebastian Ullrich
3f497b8d8e
fix(library/constructions/projection): out_params should always be implicit in projections
2018-02-02 08:58:52 -08:00
Gabriel Ebner
9920062b69
fix(kernel/expr,library/constructions/projection): preserve instance-implicitness in structure parameters
2017-08-27 16:47:04 +02:00
Gabriel Ebner
776b440d55
fix(library/constructions/projection): fix macro expansion
...
Thanks to @fpvandoorn for noticing this issue in Lean 2! We encountered
this situation when the inferred type of the projection argument did not
reduce to the structure type with the current transparency setting of
the type context.
2017-07-18 19:56:20 +01:00
Sebastian Ullrich
491802409a
chore(*): remove unused macro_definition_cell::pp method
2017-05-24 09:51:23 +02: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
d0d75c0923
refactor(kernel): reduce number of configurations supported in the kernel
...
Now, eta and impredicativity are assumed to be always true.
Motivation: the rest of the system assumes eta.
Regarding impredicativity, we decided to support only the standard library.
2016-09-27 17:07:01 -07:00
Leonardo de Moura
932d14241b
chore(kernel): remove support for mutually inductive datatypes from the kernel
2016-09-10 17:39:17 -07:00
Leonardo de Moura
81a30a69d2
refactor(library/normalize): remove unfold and unfold_full attributes
2016-09-05 08:40:58 -07:00
Leonardo de Moura
f7df7dc9a7
refactor(kernel): add reducibility_hints
2016-09-04 16:30:02 -07:00
Leonardo de Moura
f056f0f2cb
refactor(library): definitional ==> constructions
2016-08-11 10:08:22 -07:00
