<html>
<head>
<meta http-equiv="Content-Type" content="text/html; charset=UTF-8">
</head>
<body text="#000000" bgcolor="#FFFFFF">
<div class="moz-cite-prefix">On 10/16/19 4:17 AM, Artyom Shalkhakov
wrote:<br>
</div>
<blockquote type="cite"
cite="mid:CAKO6=qj8nmQCVQJUjp5fyTRTNNuB3cLowWmm8ZPE8ZqkdTim=Q@mail.gmail.com">
<meta http-equiv="content-type" content="text/html; charset=UTF-8">
<div dir="ltr">I think this is what you are looking for:<br>
<div><br>
</div>
<div><a
href="https://github.com/vizziv/UrLib/blob/master/UrLib/record.urs#L36"
moz-do-not-send="true">https://github.com/vizziv/UrLib/blob/master/UrLib/record.urs#L36</a></div>
<div><a
href="https://github.com/vizziv/UrLib/blob/master/UrLib/record.ur#L23"
moz-do-not-send="true">https://github.com/vizziv/UrLib/blob/master/UrLib/record.ur#L23</a></div>
<div><br>
</div>
<div>It would be very nice if we as a community were to come up
with a "batteries included" library for Ur/Web.<br>
</div>
</div>
</blockquote>
The equivalent code I maintain is <a moz-do-not-send="true"
href="https://github.com/achlipala/upo/blob/master/record.urs">in
UPO</a>, though I didn't bother to define this particular
operator, since, as Mark showed us, it is so directly expressed with
built-in operators.<br>
</body>
</html>