[Agda] Ill shaped metavariable?

[Nicolas Pouillard]

On Mon, 15 Nov 2010 21:34:38 +0000, Ondrej Rypacek <ondrej.rypacek at gmail.com> wrote:
> Hi, thanks for your reply. But no, I'm importing only Data.Nat

Having the type of the goal is alas not always sufficient. There is maybe
constraints implied by meta-variables that are not satisfied by your term.
If you are using the emacs interactive try to hit C-c C-= and it will display
the constraint. However they might be pretty hard to read in some cases.

Good luck,

-- 
Nicolas Pouillard
http://nicolaspouillard.fr