[racket] TR: Making recursive types as subtypes of non-recursive types

On Feb 22, 2012, at 11:12 PM, Neil Toronto wrote:

> It would be fun to try to port Coq's constructive ordinals to phantom types in TR, though, to see how far I could get with occurrence typing instead of dependent typing.


If you got far, it would validate our gut-level conjecture of 'practical dependence' for TR. 

Zermelo–Fraenkel with Choice forever :-] 

Send me a copy of the paper.