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

Do we need to learn ordinal relations in the pool #14

Closed craff closed 6 years ago

craff commented 6 years ago

Probably not. Moreover, positivity is probably useless, relation o1 < o2 are enough (as it implies o2 > 0)

But still do we need to know in the pool that o1 < o2 is true ... Probably not ?

craff commented 6 years ago

The pool is about terms and values ... ordinal are at the level of types. So the answer is no !