Stream: math-comp users

Topic: Surprising parsing of the “*l” notation


view this post on Zulip Vincent Laporte (Oct 09 2020 at 13:54):

Using Coq 8.12 and ssreflect 1.11.0, the following example surprisingly type-checks:

From mathcomp Require Import all_ssreflect.

Check forall (T lT: Type) (x: T*lT), x.1 = x.2.

Is this expected?

view this post on Zulip Cyril Cohen (Oct 09 2020 at 13:58):

Vincent Laporte said:

Using Coq 8.12 and ssreflect 1.11.0, the following example surprisingly type-checks:

From mathcomp Require Import all_ssreflect.

Check forall (T lT: Type) (x: T*lT), x.1 = x.2.

Is this expected?

Indeed, what you wrote is equivalent to:

From mathcomp Require Import all_ssreflect.

Check forall (T lT: Type) (x: T *l T), x.1 = x.2.

because *l means cartesian product with lexicographic ordering if applicable.

view this post on Zulip Vincent Laporte (Oct 09 2020 at 13:59):

But I’d expect the string T*lT to be split in the following three tokens “T”, “*”, and “lT”.

view this post on Zulip Enrico Tassi (Oct 09 2020 at 14:43):

The lexer of Coq is a beast of his own. T is the beginning and end of an IDENT, since * is not an ident char. Then *l is parsed as a symbol/keyword because it is part of a notation, and no notation has a *lT token, so it starts again and scans T as the last IDENT.
You should put a space after *l otherwise that sentence may fail to parse in the future if one adds a *lT token (hypothetical, but the warn applies in general)

view this post on Zulip Christian Doczkal (Oct 09 2020 at 14:52):

@Enrico Tassi Thank you for the explanation. Calling it a "beast" is probably right. In any event, now I understand why @Cyril Cohen insists so much on spaces around operators :grinning:

view this post on Zulip Vincent Laporte (Oct 09 2020 at 15:11):

Thanks for the explanations. So we should all put spaces around binary operators.

view this post on Zulip Enrico Tassi (Oct 09 2020 at 15:15):

Maybe we should try to implement a warning if a KEYWORD is glued to a IDENT

view this post on Zulip Cyril Cohen (Oct 09 2020 at 15:21):

Vincent Laporte said:

Thanks for the explanations. So we should all put spaces around binary operators.

And after (unary) prefix as well...

view this post on Zulip Paolo Giarrusso (Oct 09 2020 at 17:01):

@Enrico Tassi so you’d warn that *lT got parsed as *l T? Absolutely yes, please.

view this post on Zulip Paolo Giarrusso (Oct 09 2020 at 17:01):

(I wonder if having *l is a good idea, but if it is, the warning seems necessary)


Last updated: Jan 29 2023 at 18:03 UTC