[Agda] Compile-time parsing

[Peter Thiemann]

That's how I understand Conor's suggestion:
a metavariable with an empty type like T(false)
that can never be filled in.

-Peter

On 12/16/11 10:01 PM, Bengt Nordstrom wrote:
> 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
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda