[Agda] failed constraint

Andrés Sicard-Ramírez andres.sicard.ramirez at gmail.com
Tue Apr 16 22:00:41 CEST 2013


On Tue, Apr 16, 2013 at 2:47 PM, Serge D. Mechveliani <mechvel at botik.ru>wrote:

> Agda-2.3.2 MAlonzo  reports
> "
> Failed to solve the following constraints:
>   [0] Is empty: odd? .n Б┴║ true
> "
>
>
You can replace the line

odd* 0 _ _ ()

with

odd* 0 0 _ ()
odd* 0 (suc n) () _

-- 
Andrés
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.chalmers.se/pipermail/agda/attachments/20130416/85cb11a3/attachment.html


More information about the Agda mailing list