Leonardo de Moura
|
693a96681a
|
doc: fix eta struct comment
|
2021-11-26 08:36:25 -08:00 |
|
Leonardo de Moura
|
0fc8c1da77
|
feat: eta for structures at recursors
see #777
|
2021-11-25 11:31:00 -08:00 |
|
Leonardo de Moura
|
50ac21d0a6
|
refactor: move is_constructor_app to inductive.cpp
|
2021-11-25 11:31:00 -08:00 |
|
Leonardo de Moura
|
e22bffa94f
|
refactor: move is_structure_like to inductive.cpp
|
2021-11-25 11:31:00 -08:00 |
|
Leonardo de Moura
|
03e346bc66
|
chore: simplify to_cnstr_when_K
|
2021-11-25 11:31:00 -08:00 |
|
Leonardo de Moura
|
72ec0ec3ad
|
feat: string literal support on recursors and kernel isDefEq
|
2020-03-17 17:23:33 -07:00 |
|
Leonardo de Moura
|
c74f4c16ca
|
feat(library/kernel,library/compiler/csimp): make sure nat.rec and nat.cases_on reduce when major premise is a nat literal
|
2018-10-10 18:35:15 -07:00 |
|
Leonardo de Moura
|
88d4a1b0cd
|
feat(kernel/inductive): inductive_reduce_rec should not throw exception when it finds an unknown constant
It should just fail to reduce. This is important when using it in the elaborator.
|
2018-09-07 17:34:54 -07:00 |
|
Leonardo de Moura
|
58e91559d0
|
feat(*): use new inductive datatype module
|
2018-09-06 18:09:22 -07:00 |
|
Leonardo de Moura
|
10a7eccecd
|
feat(library/constructions/cases_on): add cases_on for new inductive datatype module
|
2018-09-04 09:26:16 -07:00 |
|
Leonardo de Moura
|
0285579893
|
fix(kernel/inductive): bug at inductive_reduce_rec
|
2018-09-03 17:05:13 -07:00 |
|
Leonardo de Moura
|
d325a4dd1d
|
feat(library/type_context, kernel/type_checker): use inductive_reduce_rec
|
2018-09-03 16:52:53 -07:00 |
|
Leonardo de Moura
|
799c133326
|
feat(kernel/inductive): add inductive_is_stuck
|
2018-09-03 16:06:29 -07:00 |
|
Leonardo de Moura
|
59fa70616a
|
feat(kernel/inductive): add reduce
|
2018-09-03 15:22:15 -07:00 |
|
Leonardo de Moura
|
c3c6c4afc3
|
feat(kernel/inductive): add check_inductive_types
|
2018-06-12 13:03:25 -07:00 |
|