4 commits

Author	SHA1	Message	Date
Leonardo de Moura	de48d49b53	feat(kernel): preparing for adding new inductive datatype module	2018-06-01 14:47:49 -07:00
Leonardo de Moura	ac0352b584	refactor(kernel): remove quotitent normalizer extension ... The `quot` type is now implemented in the kernel. We will do the same thing for inductives. We will not support normalizer extensions anymore in Lean4. It doesn't make sense since we settled with 2 extensions: quotients and inductives. Moreover, any new extension would require substantial changes (e.g., code generator). The normalizer_extension feature was useful when we were experimenting with different kernel flavors.	2018-06-01 10:52:17 -07:00
Nuno Lopes	ac6a16ddba	feat(msvc): further work on MSVC compatibility	2018-02-06 10:11:09 -08:00
Gabriel Ebner	2f07bf352c	refactor(library/standard_kernel): move standard kernel into kernel	2017-01-31 09:39:31 +01:00

Renamed from src/library/standard_kernel.cpp (Browse further)