Hi All,<div><br></div><div>In Haskell, if I make a record:</div><div><br></div><div>data Foo = Foo { x :: Bar, y :: Baz }</div><div><br></div><div>Then I&#39;m automatically able to &quot;set&quot; values on those records:</div>
<div><br></div><div>blerp = Foo { x = 12, y = 13 }</div><div><br></div><div>blarp = blerp { x = 13} -- y is also 13.</div><div><br></div><div>Does agda have equivalent functionality? Writing these setters manually means my code size grows quadratically in the amount of fields in the record, as I have to write:</div>
<div><br></div><div>record Blah : Set where</div><div>   field</div><div>      foo : FooT</div><div>      bar : BarT</div><div>      baz : BazT</div><div><br></div><div>   setFoo : FooT -&gt; Blah</div><div>   setFoo x = record { foo = x ; bar = bar ; baz = baz }</div>
<div><br></div><div><meta http-equiv="content-type" content="text/html; charset=utf-8"><div>   setBar : BarT -&gt; Blah</div><div>   setBar x = record { foo = foo ; bar = x ; baz = baz }</div></div><div><br></div><div><meta http-equiv="content-type" content="text/html; charset=utf-8"><div>
   setBaz : BazT -&gt; Blah</div><div>   setBaz x = record { foo = foo ; bar = bar ; baz = x }</div></div><div><br></div><div>Is there any better way to do this? Any ideas?</div><div><br></div><div>If there is no easy way to do this, how hard would it be to add such functionality to Agda? All you&#39;d have to do is (perhaps at option) generate setX functions as I have above. I might even write the patch if Agda&#39;s code is easy enough for me to figure out (I have some experience with PLs work).</div>
<div><br></div><div>Cheers.<br>~Liam<br>
</div>