search

rlepigre / pml

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

Incompleteness of typing/subtyping #32

Closed craff closed 2 years ago

craff commented 6 years ago

Here we put reference to cases were the incompleteness of typing seems not reasonable. This issue should probably never be closed.

test/fifo.pml: an annotation (x:a) is needed and this seems strange.

craff commented 2 years ago

The recent commit #66dc8347105d22265ad89a5dd55bd61ebc67f5ea alows to prove subtyping manually (this was already possible) and to use such a subtyping.