Leonardo de Moura
eab962bbc6
feat(kernel): add add_meta
2018-05-31 15:40:50 -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
7bc8673786
feat(library/module): efficient inductive_reader
...
Do not check imported inductive declarations when trust level is greater than 0.
2015-08-15 14:48:49 -07:00
Leonardo de Moura
57ea660963
refactor(*): start process for eliminating of opaque definitions from the kernel
...
see issue #576
2015-05-08 16:06:04 -07:00
Leonardo de Moura
b6781711b1
refactor(*): explicit initialization/finalization for serialization
...
modules, expression annotations, and tactics
2014-09-22 15:26:41 -07:00
Leonardo de Moura
dc503e6e3d
feat(library): add definitions_cache datastructure for implementing .clean files
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-08-10 09:53:13 -07:00
Leonardo de Moura
0779db7ae9
fix(kernel): set module_idx on theorems, otherwise we are not able to import theorems that use opaque definitions
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-06-16 16:56:11 -07:00
Leonardo de Moura
49e1f78a33
feat(library/kernel_serializer): add serializer/deserializer for inductive decls
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-05-26 15:37:53 -07:00
Leonardo de Moura
8872d4a531
refactor(kernel): rename definition class to declaration
...
The name was misleading since not every declaration is a definition.
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-05-20 10:41:38 -07:00
Leonardo de Moura
c0d8a3195c
fix(library/kernel_serializer): style
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-05-15 18:00:09 -07:00
Leonardo de Moura
660b9299ad
refactor(kernel): (de)serialization procedures don't need to be in the kernel
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-05-15 17:23:36 -07:00
