rlepigre / pml

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

Deal with unification variables after type-checking (mantis #44) #16

Open craff opened 6 years ago

craff commented 6 years ago

Unification variable that remains after type-checking should get a default instanciation.

Remark: if later we keep unification constraints, this would become very important as there could be unsolvable contraints, or preferably, we should ensure all constraints have a default instanciation that we could use.