I answer to myself XD<br>For some reason, Agda cannot see that the definitions are terminating ( but i think they are!), and this is why the highlighting. <br>Thank you.<br><br><div class="gmail_quote">2010/7/17 Leonardo Rodriguez <span dir="ltr"><<a href="mailto:leonardomatiasrodriguez@gmail.com">leonardomatiasrodriguez@gmail.com</a>></span><br>
<blockquote class="gmail_quote" style="border-left: 1px solid rgb(204, 204, 204); margin: 0pt 0pt 0pt 0.8ex; padding-left: 1ex;">I'm trying to write mutual recursive functions using the "mutual" clause. But<br>
when Agda loads the program, the operators ↓≤ and ↑≤ are hightlighted in orange and<br>the "Checked" message does not appear. What's the problem? <br>
<br>mutual<br> _↓≤_ : Simple -> Simple -> Bool<br> ...definition uses ↑≤...<br><br> _↑≤_ : Type -> Type -> Bool<br> ...definition uses ↓≤...<br><br>Thanks you in advance<br><br>
</blockquote></div><br>