Dear Agda Users,<br><br>I have noticed that when defining functions in a record they are not <br>termination checked. Below is a small module that passes the <br>type checking.<br><br>If function f is taken out of the record then the termination checker<br>
picks it up. Presumably because the record definition creates a new<br>module so feedback is not given in the original definition.<br><br>I have tested this in the latest development version, checked out<br>3rd November. Also, have taken a quick look over the bug reports<br>
and not seen any mention of it.<br><br><br>module error where<br><br>record A : Set where<br>  field<br>    a : A<br><br>  f : A → A<br>  f = f<br><br><br>I assume this is not the intended behaviour?<br><br>Regards,<br>Karim Kanso<br>