Fabrício S. Paranhos (Mar 09 2021 at 14:24): Fabrício S. Paranhos (Mar 09 2021 at 14:24):Hello, I'm trying to define a notation (unicode symbol) to a class:
Class T {A: Type} := t: A.
The symbol "∅" works fine:
Notation "∅" := t (format "∅").
But, when defining with a different symbol, Coq (8.12.2) expect an explicit level:
Fail Notation "ψ" := t (format "ψ").
The command has indeed failed with message:
A left-recursive notation must have an explicit level.
Why? Thanks!
Théo Winterhalter (Mar 09 2021 at 14:28):I think it's because here your symbol can be used as a variable name, while the empty set wouldn't be accepted.
You can specify that you mean to use it as a symbol with single quotes:
Notation "'ψ'" := (t) (format "ψ").
I guess someone already defined the level of It is a pity to make a keyword out of such symbols that are commonly used as variables..."∅" but not the one of "ψ".
Cyril Cohen (Mar 09 2021 at 14:30):I think Notation ψ := t. should be preferred...
Théo Winterhalter (Mar 09 2021 at 14:31):Cyril Cohen said:
I think
Notation ψ := t.should be preferred...
Because it doesn't update the lexer/parser, while Notation with quotes does, right?
Cyril Cohen (Mar 09 2021 at 14:32):Right, writing
Notation "'ψ'" := (t) (format "ψ").
will contaminate dependencies and make the use of ψ as a variable impossible.
Cyril Cohen (Mar 09 2021 at 14:35):Goal forall ψ : nat, ψ = 0. Abort. (* OK *)
Notation "'ψ'" := 0 (format "ψ").
Goal forall ψ : nat, ψ = 0. (* Syntax error *)
Théo and Cyril, thanks for the replies. I forgot to supply a minimal example:
Class T {A: Type} := t: A.
Class J {A: Type} := j: A.
Notation "∅" := t.
Fail Notation "ψ" := j.
This behavior is really strange, why is "∅" treated differently then "ψ" or any other symbol? I should mention that I'm running this without any theory, even Init.Prelude (-noinit).
Cyril Cohen said:
I think
Notation ψ := t.should be preferred...
Notation ψ := j. works fine, but Notation ∅ := t. fails with Error: Syntax Error: Lexer: Undefined token.
Guillaume Melquiond (Mar 09 2021 at 16:52):It might be that one of the two symbols is incorrectly classified in the unicode tables used by Coq.
Guillaume Melquiond (Mar 09 2021 at 16:56):So, they are correctly classified: The first one is a "mathematical symbol", while the second one is a "lowercase letter".
Guillaume Melquiond (Mar 09 2021 at 17:00):And Coq does not allow symbols to start identifiers, hence why they are treated differently.
Fabrício S. Paranhos (Mar 11 2021 at 12:27):Guillaume, thanks for clarifying!
Last updated: Oct 04 2023 at 19:01 UTC