search

wilbowma / cur

A less devious proof assistant
BSD 2-Clause "Simplified" License
222 stars 18 forks source link

Transitivity of subtyping? #47

Closed wilbowma closed 4 years ago

wilbowma commented 8 years ago

I think transitivity of subtyping is broken. See http://www.cse.chalmers.se/~ulfn/papers/thesis.pdf for how to actually implement this.

maxsnew commented 8 years ago

Counterexample?

wilbowma commented 8 years ago

Wouldn't be a question if I had one; I suspect it though due to my hasty adaptation of declarative conversion rule into algorithmic rules, and due to similar bug in my cic-redex model.

stchang commented 4 years ago

Yes I think subtyping is working. Closing until someone comes up with a specific counterexample.