[Agda] failed constraint
Serge D. Mechveliani
mechvel at botik.ru
Fri Apr 19 09:27:14 CEST 2013
On Tue, Apr 16, 2013 at 03:00:41PM -0500, Andr??s Sicard-Ram??rez wrote:
> 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:
> >  Is empty: odd? .n Б┴║ true
> > "
> You can replace the line
> odd* 0 _ _ ()
> odd* 0 0 _ ()
> odd* 0 (suc n) () _
This helps. Thank you.
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.
2) The work around like splitting, for example,
odd* 0 _ _ ()
to several clauses by the second argument leads to an unnecessary
Also after this "Failed to solve", one needs to find: which clause in
a large module needs to be split.
More information about the Agda