On 10/16/19 4:17 AM, Artyom Shalkhakov wrote:
I think this is what you are looking for:
https://github.com/vizziv/UrLib/blob/master/UrLib/record.urs#L36
https://github.com/vizziv/UrLib/blob/master/UrLib/record.ur#L23
It would be very nice if we as a community were to come up with a
"batteries included" library for Ur/Web.
The equivalent code I maintain is in UPO
<https://github.com/achlipala/upo/blob/master/record.urs>, though I
didn't bother to define this particular operator, since, as Mark showed
us, it is so directly expressed with built-in operators.
_______________________________________________
Ur mailing list
Ur@impredicative.com
http://www.impredicative.com/cgi-bin/mailman/listinfo/ur
