[Agda] Mutual clause
Leonardo Rodriguez
leonardomatiasrodriguez at gmail.com
Sat Jul 17 20:56:07 CEST 2010
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/b01b4dbc/attachment.html
More information about the Agda
mailing list