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!

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 `"ψ"`

.

I think `Notation ψ := t.`

should be preferred...

Cyril Cohen said:

I think

`Notation ψ := t.`

should be preferred...

Because it doesn't update the lexer/parser, while `Notation`

with quotes does, right?

Right, writing

```
Notation "'ψ'" := (t) (format "ψ").
```

will contaminate dependencies and make the use of `ψ`

as a variable impossible.

```
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`

.

It might be that one of the two symbols is incorrectly classified in the unicode tables used by Coq.

So, they are correctly classified: The first one is a "mathematical symbol", while the second one is a "lowercase letter".

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

Guillaume, thanks for clarifying!

Last updated: Jun 24 2024 at 12:02 UTC