We should be able to use constraint ordering on ordinals.

rlepigre / pml

New version of the PML language and (classical) proof assistant

http://pml-lang.org

MIT License

20 stars 2 forks source link

Open craff opened 2 years ago

craff commented 2 years ago

This is needed to write subtyping proof manually (and checking termination giving exact induction hyp). Need a use case first ?