[Agda] failed constraint

[Nils Anders Danielsson]

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
(http://code.google.com/p/agda/issues/detail?id=835).

> 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.

-- 
/NAD