Permalink
Switch branches/tags
Nothing to show
Find file
Fetching contributors…
Cannot retrieve contributors at this time
6 lines (5 sloc) 269 Bytes
- should be a good idea to add the fact that a constante is reducible or not, or even its nature
- adding well-formness
+ Universe stratification
+ Type stratification (* alternatives to positivity *)
+ Proof Irrelevance (should extend the unification algorithm)