rlepigre / pml

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

Add a syntaxtic sugar to extend record. #40

Open craff opened 2 years ago

craff commented 2 years ago

Minimal syntactic { include r1; include r2; ... } should use typing to know the field that are present. The same notation for type is just some kind of higher order function performing some computation on type.

The general include for a record of unknown type (or default record value) seems too hard at the moment, especially for compilation.