[Agda] updating record field

Sergei Meshveliani mechvel at botik.ru
Sun Feb 2 13:18:20 CET 2014


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



More information about the Agda mailing list