[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"
> 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:
 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