rlepigre / pml

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

auto cases! use information from typing #30

Open craff opened 6 years ago

craff commented 6 years ago

Some time, extra information comes from typing which allows to restrict cases. This information is probably available in the type of the VWit ... We should try to use it!

See lib/int.pml for a use case.