Better control of current totality status

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 6 years ago

craff commented 6 years ago

When writing let f = fun x ... or even applications, or dependant product, we have no short way to indicate the current totality we want.

Do we need something (like more than one keyword for fun ?)

craff commented 6 years ago

Moved to project

craff commented 6 years ago

Reopen as the is a FIXME in the code : we have notation for the arrow: ~>, -> and => But we only have one dependant product!

craff commented 6 years ago

A use case is in