[Agda] Compile-time parsing

[Nils Anders Danielsson]

On 2011-12-15 12:35, Andres Löh wrote:
> I don't understand completely why you're opposed to your first
> solution. Code being highlighted in yellow *is* a (particular kind of)
> type error in Agda. In fact, it's a particularly well-behaved kind of
> type error from which the type checker can recover and still check the
> rest of the program. There's no implication that yellow means "almost
> correct" ...

At the last AIM Nicolas Pouillard suggested that unsolved meta-variables
should (by default) be treated as errors. I think his main motivation
was that type-checking can be very slow if you have an unsolved
meta-variable at the top of a long file. What do you think of this?

(I'm not sure how easy this would be to implement, given that
meta-variables related to goals should not be treated as errors.)

-- 
/NAD