Marc Weber wrote:
something more funny does no longer work:con change_name_toggle :: Name -> Name = fn name => case name of #Boo => #Bar |#Bar => #Boo
Yes, unlike Agda, Ur has separate languages for compile-time and run-time code. You are trying to define a compile-time thing but using syntax that is only allowed for run-time code.
So is there any way (more than one) to implement such function?
I certainly hope not; that would break a nifty language property called "parametricity" which lets us deduce some specific properties of programs from their types.
What else can be done with names? There are no operations such as "prefix them with db_" or such, are there?
Correct. The grammar of constructors in the manual gives a complete catalog of operations.
_______________________________________________ Ur mailing list [email protected] http://www.impredicative.com/cgi-bin/mailman/listinfo/ur
