Hello guys, I've recently started studying type theory hoping to use it for my computational biology thesis. I'm quite interested in its practical applications and Ur as an example of such.
Can anyone tell where in the lambda cube falls Ur's type system? I understand that it is not a fully dependently typed system, but what's missing? Type-level unions maybe? Alex _______________________________________________ Ur mailing list [email protected] http://www.impredicative.com/cgi-bin/mailman/listinfo/ur
