[Agda] Mutual clause

[Leonardo Rodriguez]

I answer to myself XD
For some reason, Agda cannot see that the definitions are terminating ( but
i think they are!), and this is why the highlighting.
Thank you.

2010/7/17 Leonardo Rodriguez <leonardomatiasrodriguez at gmail.com>

> I'm trying to write mutual recursive functions using the "mutual" clause.
> But
> when Agda loads the program, the operators ↓≤ and ↑≤  are hightlighted in
> orange and
> the "Checked" message does not appear. What's the problem?
>
> mutual
>   _↓≤_ : Simple -> Simple -> Bool
>   ...definition uses ↑≤...
>
>   _↑≤_ : Type -> Type -> Bool
>   ...definition uses ↓≤...
>
> Thanks you in advance
>
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.chalmers.se/pipermail/agda/attachments/20100717/9f1fbcbd/attachment.html