Leonardo de Moura
f9d87e7a98
feat(kernel/inductive): add inductive postprocessor
...
We still need to restore recursors and their rules
2018-09-02 17:44:19 -07:00
Leonardo de Moura
41a87f6856
feat(kernel/inductive): normalize parameter names
2018-09-02 16:40:31 -07:00
Leonardo de Moura
7d4097818b
feat(kernel/inductive): add recursor rules
2018-09-02 15:55:29 -07:00
Leonardo de Moura
f30cb0635f
chore(kernel/inductive): cleanup
2018-09-02 09:26:58 -07:00
Leonardo de Moura
98f035088c
chore(kernel/inductive): cleanup
2018-08-31 18:01:26 -07:00
Leonardo de Moura
517923d362
feat(kernel/inductive): generate recursors in the new inductive datatype module
2018-08-31 17:47:22 -07:00
Leonardo de Moura
2fb677f1d0
feat(kernel/inductive): add positivity check to new inductive datatype module
2018-08-31 09:52:38 -07:00
Leonardo de Moura
706d7045c3
feat(kernel/inductive): add nested => mutual preprocessor
2018-08-30 18:05:43 -07:00
Leonardo de Moura
f1105e108a
fix(kernel/inductive): bug at check_inductive_types
2018-08-30 18:05:43 -07:00
Leonardo de Moura
863355c6a0
feat(kernel/inductive): continue new inductive datatype module
...
Add more validation, and create new inductive_val and constant_val objects.
2018-08-29 09:27:06 -07:00
Leonardo de Moura
d1d56776ad
feat(kernel): invoke add_inductive for inductive datatype declarations
2018-08-28 15:54:46 -07:00
Leonardo de Moura
82095cc018
refactor(kernel): split declaration into declaration and constant_info
...
This is just another step towards the design described at commit 16598391a07d4a
2018-08-22 17:53:11 -07:00
Leonardo de Moura
9d35d31529
refactor(kernel): merge constant_assumption and axiom
2018-08-01 09:57:47 -07:00
Leonardo de Moura
bda46cc9ac
feat(kernel): add inductive_decl type on top of runtime/object, and ajust kernel/inductive.cpp
2018-06-26 12:16:33 -07:00
Leonardo de Moura
bc57c66ae3
refactor(kernel/level): naming consistency
2018-06-22 10:29:56 -07:00
Leonardo de Moura
e590ebf54d
feat(kernel/inductive): initialize m_elim_level
2018-06-12 15:17:52 -07:00
Leonardo de Moura
effefb8b03
chore(kernel/inductive): style
2018-06-12 13:03:25 -07:00
Leonardo de Moura
5088252aa8
feat(kernel): add proper constructor struct
2018-06-12 13:03:25 -07:00
Leonardo de Moura
c3c6c4afc3
feat(kernel/inductive): add check_inductive_types
2018-06-12 13:03:25 -07:00
Leonardo de Moura
a632df3211
refactor(kernel/inductive): do not use ginductive inductive declaration format
...
The format used by ginductive is more compact, but it forces the kernel
to implement the `infer_implicit_params`. It would also create problems
when we make inductive_decls a special case of declaration
2018-06-11 12:52:44 -07:00
Leonardo de Moura
818170d780
refactor(kernel): remove tag from kernel expressions
...
We are temporarily storing position information in a global table.
2018-06-08 10:29:22 -07:00
Leonardo de Moura
2a79da1ab6
refactor(kernel): move formatting stuff out of the kernel
2018-06-07 16:28:54 -07:00
Leonardo de Moura
3d38923e07
feat(frontends/lean/inductive_cmds): add option for invoking future inductive module
2018-06-01 16:25:21 -07:00
Leonardo de Moura
de48d49b53
feat(kernel): preparing for adding new inductive datatype module
2018-06-01 14:47:49 -07:00
