'#Other' means a _name_ of field, but the (~) checks if two _sets_ of fields
have empty intersection.
The right syntax is like:
$ cat ab.ur
fun join [record] [other] [ [Other] ~ record ] (r:$record) (f:other) =
r ++ { Other = f }
val tst = join {} 1
$ cat ab.urs
val join : record ::: {Type} -> other ::: Type -> [ [Other] ~ record ] =>
$record -> other -> $(record ++ [ Other = other ])
23.02.2012, 19:02, "Gergely Buday" <[email protected]>:
> Hi,
>
> I am trying to code a simple function that augments a record with an {
> Other : other } field. What am I doing wrong?
>
> $ cat implicit.urs
> val join : record ::: {Type} -> other ::: Type -> [ #Other ~ record ] =>
> $record -> other -> $(record ++ [ Other = other ])
>
> $ cat implicit.ur
> fun join [record] [other] [ #Other ~ record ] (r:$record) (f:other) =
> r ++ { Other = f }
_______________________________________________
Ur mailing list
[email protected]
http://www.impredicative.com/cgi-bin/mailman/listinfo/ur
