[Ur] Which is the syntax for record updating

[Gabriel Riba]

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.