Stream: Coq users

Topic: Notation fail with different symbols (utf8)


view this post on Zulip 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!

view this post on Zulip 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 "ψ").

view this post on Zulip Cyril Cohen (Mar 09 2021 at 14:29):

I guess someone already defined the level of "∅" but not the one of "ψ". It is a pity to make a keyword out of such symbols that are commonly used as variables...

view this post on Zulip Cyril Cohen (Mar 09 2021 at 14:30):

I think Notation ψ := t. should be preferred...

view this post on Zulip 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?

view this post on Zulip 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.

view this post on Zulip Cyril Cohen (Mar 09 2021 at 14:35):

Goal forall ψ : nat, ψ = 0. Abort. (* OK *)
Notation "'ψ'" := 0 (format "ψ").
Goal forall ψ : nat, ψ = 0. (* Syntax error *)

view this post on Zulip Fabrício S. Paranhos (Mar 09 2021 at 16:39):

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.

view this post on Zulip 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.

view this post on Zulip 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".

view this post on Zulip Guillaume Melquiond (Mar 09 2021 at 17:00):

And Coq does not allow symbols to start identifiers, hence why they are treated differently.

view this post on Zulip Fabrício S. Paranhos (Mar 11 2021 at 12:27):

Guillaume, thanks for clarifying!


Last updated: Feb 06 2023 at 13:03 UTC