Automatic case analysis (mantis #34)

rlepigre / pml

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

http://pml-lang.org

MIT License

20 stars 2 forks source link

Automatic case analysis (mantis #34) #19

Closed craff closed 6 years ago

craff commented 6 years ago

Perform a case analysis based on blocked case in evaluation. Could also do case analysis convergent/non convergent (pml1 does it)

craff commented 6 years ago

This will also be useful for missing totalities. If f (g x) is blocked in the pool because g x is not a value, pml can try to type-check g x to get its totality.

craff commented 6 years ago

Done, remain issue #28 and #29 ... That can wait a bit