[Agda] failed constraint

Nils Anders Danielsson nad at cse.gu.se
Fri Apr 19 11:54:55 CEST 2013

On 2013-04-19 09:27, Serge D. Mechveliani wrote:
> Dear Agda developers,
> is it possible to fix these  "Failed to solve ... constraints"
> reports?
> 1) They do not locate the place, do not help to fix a program.

I get the following error message:

   Failed to solve the following constraints:
     [0] Is empty: odd? .n ≡ true
         [ at /tmp/Main.agda:22,18-20 ]

The error location is not printed in the Emacs interface, though. I've
created a ticket for this issue

> 2) The work around like splitting, for example,
>                                                 odd* 0 _ _ ()
>     to several clauses by the second argument leads to an unnecessary
>     complicated program.

This is a separate issue. I don't think we should add some "magic"
emptiness search to Agda.


More information about the Agda mailing list