data U0: Type =
int: U0
text: U0
option: U0 -> U0
interpret (u: U0): Type =
case u of
U0.int => Int
U0.text => Text
U0.option \u => Option (interpret u)
We might want to have some syntactic sugar like this:
@(universe interpret)
data U0: Type =
int = Int
text = Text
option = Option
Instead of this kind of boilerplate:
We might want to have some syntactic sugar like this: