<br><div class="gmail_quote">On Tue, Apr 16, 2013 at 2:47 PM, Serge D. Mechveliani <span dir="ltr">&lt;<a href="mailto:mechvel@botik.ru" target="_blank">mechvel@botik.ru</a>&gt;</span> wrote:<br><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">

Agda-2.3.2 MAlonzo  reports<br>
&quot;<br>
Failed to solve the following constraints:<br>
  [0] Is empty: odd? .n Б┴║ true<br>
&quot;<br>
<br></blockquote><div><br>You can replace the line<br><br>odd* 0 _ _ ()<br><br>with<br><br>odd* 0 0 _ ()<br>odd* 0 (suc n) () _<br clear="all"></div></div><br>-- <br>Andrés<br>