[Agda] Compile-time parsing

[Bengt Nordstrom]

I look at a metavariable as a part of an expression which is not
filled in yet. So an expression with
a metavariable is not erroneous, it is just not yet complete. It would
be erroneous if it is impossible
to fill it in.

Or do you have some special interpretation of the word "erroneous"?

Best regards,
Bengt

On Fri, Dec 16, 2011 at 11:13 AM, Conor McBride
<conor at strictlypositive.org> wrote:
>
> On 16 Dec 2011, at 10:03, Nils Anders Danielsson wrote:
>
>> 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.)
>
>
> How about treating as an error an unsolved meta whose type, were it an
> hypothesis, would be dismissed by an absurd pattern?
>
> Conor_______________________________________________
>
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda