Adam Chlipala wrote:
That's about the simplest syntax there is at the moment, though it is
also possible to define a library function that hides use of the [---]
operator to make the syntax a bit more compact.
fun overwrite [a] [b] [a ~ b] (r : $(a ++ b)) (r' : $b) : $(a ++ b) =
r --- b ++ r'
val test = overwrite {A = 1, B = "", C = 2.3} {A = 8, C = 4.5}
Thanks a lot.
This works if the target record type is the original one
but not when I map a field value to a different type.
Although I've found a solution:
fun overwrite [a] [b] [b'] [a ~ b] [a ~ b'] (r : $(a ++ b)) (r' : $b') :
$(a ++ b') =
r --- b ++ r'
Maybe a function of this kind should belong to the Ur predefined
functions module.
_______________________________________________
Ur mailing list
[email protected]
http://www.impredicative.com/cgi-bin/mailman/listinfo/ur
