defining record types with overloaded functions on universally quantified variables
It would be convenient to be able to define a record type such as:
:: T = { f :: A.a: a -> a | == a }
It would be convenient to be able to define a record type such as:
:: T = { f :: A.a: a -> a | == a }