[Agda] Unsolved metas

[Christoph Herrmann]

Hi

On 10 Feb 2011, at 00:01, Permjacov Evgeniy wrote:

> When I try to typecheck some of my code in batch mode, Agda reports
> about unsolved metas and terminates. What does it (unsolved metas) mean 

This means the type checker cannot verify type correctness, but also cannot
construct a contradiction such as zero /= suc

> and is there any reason to not supress this with --allow-unsolved-metas
> option ?

Well, if there actually is an error, your program will be incorrect.
I assume that is reason enough ;-)

If it is correct, I assume there still might be a problem concerning 
generation of correct code, if the code generator does not get
a consistent view of the types of the subexpressions.

Cheers
--
 Dr. Christoph Herrmann
 University of St Andrews, Scotland/UK
 phone: office: +44 1334 461629, home: +44 1334 478648 
 email: ch at cs.st-andrews.ac.uk,  c.herrmann at virgin.net
 URL:   http://www.cs.st-andrews.ac.uk/~ch
 
 The University of St Andrews is a charity registered in Scotland: No SC013532