[Agda] updating record field

[Ulf Norell]

Yes,

  r' = record r { foo1 = x; foo3 = y }

/ Ulf


On Sun, Feb 2, 2014 at 1:18 PM, Sergei Meshveliani <mechvel at botik.ru> wrote:

> People,
>
> Suppose that  record Foo ...
>
> has 8 fields  foo1, ..., foo8,
> and
>       r : Foo.
>
> How to express that  r'  is obtained from  r  by updating the field
> values for  foo1 and foo3  only?
>
> Is this possible without rewriting the other 6 fields in the code?
>
> Thanks,
>
> ------
> Sergei
>
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.chalmers.se/pipermail/agda/attachments/20140203/4d8eaa0d/attachment.html