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. ____________________ Racket Users list: http://lists.racket-lang.org/users
