[Agda] Compile-time parsing

Nils Anders Danielsson nad at chalmers.se
Fri Dec 16 13:14:18 CET 2011


On 2011-12-16 12:39, Conor McBride wrote:
> PS In the presence of equality on sets, where coercion between
> provably equal sets is definable, it is possible to replace very
> many type errors by irredeemable metavariables, turning brown to
> yellow.

What are you referring to here?

-- 
/NAD


More information about the Agda mailing list