Leonardo de Moura
|
ca0c205389
|
feat: add registerSimpAttr
|
2021-08-16 09:59:58 -07:00 |
|
Leonardo de Moura
|
3c68703f39
|
feat: elaborate <- modifier at simp arguments
|
2021-08-15 07:07:58 -07:00 |
|
Leonardo de Moura
|
4062dee864
|
fix: fixes #498
|
2021-05-31 15:42:13 -07:00 |
|
Leonardo de Moura
|
0f43a338e6
|
feat: improve error message
|
2021-05-14 18:05:04 -07:00 |
|
Leonardo de Moura
|
05147fd352
|
fix: do not generate injectivity theorems for unsafe inductive datatypes
|
2021-05-14 18:05:04 -07:00 |
|
Leonardo de Moura
|
175311b2f0
|
feat: avoid trivial injectivity theorems
|
2021-05-14 18:05:04 -07:00 |
|
Leonardo de Moura
|
112bb0ed79
|
fix: injectivity theorem for constructors with dependent fields
|
2021-05-14 18:05:04 -07:00 |
|
Leonardo de Moura
|
f850820029
|
feat: add mkInjectiveTheorems
|
2021-05-13 22:09:50 -07:00 |
|