search

rlepigre / pml

New version of the PML language and (classical) proof assistant
http://pml-lang.org
MIT License
20 stars 2 forks source link

Mutually inductive types #13

Open craff opened 6 years ago

craff commented 6 years ago

Mutually inductive types can be encoded using extra parameters, but this result in a notion of sized type which is not the one we want, and leads to failure of the termination checker.