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>