Leonardo de Moura
ac87de33e7
fix(frontends/lean/structure_cmd): universe level validation in the structure command
2016-09-18 10:00:31 -07:00
Leonardo de Moura
6c84a0a7b1
feat(frontends/lean): use new notation for declaring universes in constant and structure decls
2016-09-13 21:45:16 -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
Daniel Selsam
b0c5744eea
feat(inductive_compiler): support for mutually inductive types
2016-09-10 14:22:27 -07:00
Leonardo de Moura
8d9e508a11
fix(frontends/lean/structure_cmd): leftover
2016-09-10 12:57:24 -07:00
Leonardo de Moura
d8caecff49
refactor(library/exception): avoid throw_generic_exception functions
2016-09-06 12:37:56 -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
a93eada058
feat(library/type_context): improved (and simplified) cache management for type_context
2016-08-23 17:56:58 -07:00
Leonardo de Moura
423319398d
fix(frontends/lean/structure_cmd): compilation warning
2016-08-17 15:42:20 -07:00
Daniel Selsam
a9b01991c2
feat(frontends/lean/inductive_cmd): new frontend for the inductive cmd
...
Conflicts:
src/frontends/lean/CMakeLists.txt
src/frontends/lean/structure_cmd.h
2016-08-17 07:34:03 -07:00
Leonardo de Moura
4e0a30d21e
chore(frontends/lean/structure_cmd): remove unnecessary dependency
2016-08-16 14:58:13 -07:00
Leonardo de Moura
e384b5c5f9
refactor(frontends/lean): move structure_instance to separate module
2016-08-16 14:56:09 -07:00
Leonardo de Moura
f056f0f2cb
refactor(library): definitional ==> constructions
2016-08-11 10:08:22 -07:00
Leonardo de Moura
53aa89f1e1
fix(frontends/lean/structure_cmd): generate code for automatically generated coercions
2016-08-08 13:58:34 -07:00
Leonardo de Moura
1041f6d9d8
feat(frontends/lean/structure_cmd): private structures
2016-08-06 00:03:06 -07:00
Leonardo de Moura
46570bd51d
fix(frontends/lean/structure_cmd): bug when generating alias for S.induction_on in the structure command
2016-08-05 23:13:39 -07:00
Leonardo de Moura
aeafe0293b
feat(frontends/lean/structure_cmd): use new elaborator to process the structure command
2016-08-03 16:56:41 -07:00
Leonardo de Moura
d473622352
refactor(frontends/lean/structure_cmd): remove unnecessary options
2016-08-03 15:48:58 -07:00
Leonardo de Moura
0169989411
chore(library/class): remove transitive instance support
...
Conflicts:
src/frontends/lean/structure_cmd.cpp
src/library/class.cpp
src/library/class.h
2016-07-29 23:32:10 -07:00
Sebastian Ullrich
c4edad0372
feat(frontends/lean, library): remove attribute and metaclass scoping
...
All data is now part of either a global, permanent scope or a local,
temporary one
2016-07-29 23:44:21 -04:00
Leonardo de Moura
a64d1a77ea
refactor(library, frontends/lean): remove old coercion management module
2016-07-29 13:51:26 -07:00
Leonardo de Moura
7a92ce38bd
refactor(frontends/lean): elaborator_exception ==> old_elaborator_exception
2016-07-26 16:24:28 -07:00
Sebastian Ullrich
c5a8fe02ac
feat(frontends/lean): add parent classes to local context in struct definitions
...
Fixes #1066
2016-07-05 19:22:08 -07:00
Daniel Selsam
aabdabdb17
fix(src/frontends/lean/structure_cmd): fixes #1036
2016-06-14 17:52:31 -07:00
Daniel Selsam
4fdf608c36
fix(src/frontends/lean/structure_cmd): check if indices are provided
2016-06-14 17:52:19 -07:00
Sebastian Ullrich
9561b45af1
fix(frontends/lean): uniform handling of declaration compound names
...
* allow compound names in `namespace` and `structure`
* adjust error messages
Conflicts:
src/frontends/lean/builtin_tactics.cpp
2016-06-02 18:13:50 -07:00
Leonardo de Moura
df0d39ccee
feat(kernel,library/definitional,frontends/lean/structure_cmd): make sure we can define inductive datatypes and structures containing untrusted declarations
...
If they contain untrusted declarations, then the associated
declarations (e.g., constructors) will be automatically tagged as untrusted.
2016-06-02 16:19:06 -07:00
Leonardo de Moura
dd4d115cc5
fix(frontends/lean/structure_cmd): mark recursors generated by structure cmd as auxiliary
2016-05-11 14:18:29 -07:00
Leonardo de Moura
c4f25cf15b
refactor(frontends/lean): rename elaborate methods
2016-03-30 15:05:24 -07:00
Leonardo de Moura
487a1e7f89
refactor(kernel): remove extension_context
...
We replaced it with abstract_type_context
2016-03-19 15:15:39 -07:00
Leonardo de Moura
e7f1f409c4
refactor(kernel): simplify kernel type_checker
...
TODO: cleanup, move justification/metavar/constraints to library
2016-03-18 16:28:42 -07:00
Leonardo de Moura
d8079aa16a
refactor(library): create copy of the kernel type_checker in library
...
Motivation: it will allow us to simplify the kernel type_checker and
make sure it implements the same API provided by type_context
2016-03-18 14:34:10 -07:00
Leonardo de Moura
146edde5b3
feat(library/class): mark instances as quasireducible by default
...
quasireducible are also known as lazyreducible.
There is a lot of work to be done.
We still need to revise blast, and add a normalizer for type class
instances. This commit worksaround that by eagerly unfolding
quasireducible.
2016-02-25 12:11:29 -08:00
Leonardo de Moura
96f391dda2
feat(library/definitional/projection,frontends/lean/structure_cmd): creating inductive predicates using structure command
2016-02-22 16:09:44 -08:00
Leonardo de Moura
c9e9fee76a
refactor(*): remove name_generator and use simpler mk_fresh_name
2016-02-11 18:05:57 -08:00
Leonardo de Moura
a08bc408c8
fix(frontends/lean/structure_cmd): fixes #967
2016-02-04 16:15:18 -08:00
Leonardo de Moura
31cc0ebb6a
fix(frontends/lean/structure_cmd): fixes #968
2016-02-04 15:45:38 -08:00
Leonardo de Moura
ce622e9179
feat(frontends/lean): add auto-include for structures and inductive decls
2015-12-13 13:39:34 -08:00
Leonardo de Moura
cf61adc5d5
feat(frontends/lean): identifiers starting with '_' are now reserved
2015-12-10 22:32:03 -08:00
Leonardo de Moura
e5aab3fd63
feat(library/scoped_ext,frontends/lean): add support for setting attributes into different namespaces
2015-12-05 11:15:02 -08:00
Leonardo de Moura
9bedbbb739
refactor(library,hott): remove coercions between algebraic structures
...
They are classes, and mixing coercion with type class resolution is a
recipe for disaster (aka counterintuitive behavior).
2015-11-11 11:57:44 -08:00
Leonardo de Moura
45163acf25
refactor(kernel/inductive): use local constants to represent introduction rules
2015-08-25 03:46:28 -07:00
Leonardo de Moura
26574e29a9
feat(library/normalize,frontends/lean): allow multiple arguments in [unfold] hint
...
closes #693
2015-07-07 18:01:57 -07:00
Leonardo de Moura
4b1b3e277f
feat(frontends/lean): rename '[unfold-c]' to '[unfold]' and '[unfold-f]' to '[unfold-full]'
...
see issue #693
2015-07-07 16:37:06 -07:00
Leonardo de Moura
4ae9f3ea81
feat(library/coercion): new coercion manager
...
closes #668
2015-07-01 16:32:34 -07:00
Leonardo de Moura
859ef441a0
feat(library/class): transitive instances
...
see issue #666
2015-06-27 14:06:56 -07:00
Leonardo de Moura
0b7859f387
feat(library,frontends/lean): add support for projections in the elaborator
...
The idea is to simulate the computation rules such as
pr1 (mk a b) ==> a
in the elaborator
2015-06-26 17:18:29 -07:00
Leonardo de Moura
1c70514231
feat(frontends/lean/structure_cmd): disable conversion optimization for automatically generated coercions
2015-06-21 16:57:37 -07:00
Leonardo de Moura
d0d3f9bb41
refactor(kernel,library,frontends/lean): add helper functions, and cleanup collect_locals
2015-06-05 17:29:36 -07:00
