[Agda] Agdas constraint solver too eager?!

Nils Anders Danielsson nad at chalmers.se
Sun Sep 9 11:05:04 CEST 2012


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


More information about the Agda mailing list