[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