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?
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.
But I’d expect the string T*lT
to be split in the following three tokens “T”, “*”, and “lT”.
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)
@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:
Thanks for the explanations. So we should all put spaces around binary operators.
Maybe we should try to implement a warning if a KEYWORD is glued to a IDENT
Vincent Laporte said:
Thanks for the explanations. So we should all put spaces around binary operators.
And after (unary) prefix as well...
@Enrico Tassi so you’d warn that *lT
got parsed as *l T
? Absolutely yes, please.
(I wonder if having *l
is a good idea, but if it is, the warning seems necessary)
Last updated: Oct 13 2024 at 01:02 UTC