[Agda] Agdas constraint solver too eager?!

[Nils Anders Danielsson]

On 2012-09-09 07:57, Ulf Norell wrote:
> This is the correct behaviour. Your assertion that 'false' would be a
> solution is incorrect.

Good point.

> We've had this discussion before. Metavariables are solved with unique
> solutions that make the intensional equality hold, not the extensional
> equality.

Both Andreas and I have made this mistake before. Please keep reminding
us. :)

-- 
/NAD