Positivity is a common restriction when defining inductive types in type-theory based proof assistants.
References:
Counterexamples in Type Systems - Positivity, strict and otherwise
About
Stats
|
created |
2 years, 3 months ago |
|
viewed |
7 times |
|
active |
2 years, 3 months ago |
|
editors |
1 |
