cc @Hugo Herbelin

I can't get the following custom notation to print. It is being parsed fine however:

```
Axiom FOTerm : Type.
Axiom FOFormula : Type.
Axiom fo_bot : FOFormula.
Axiom fo_top : FOFormula.
Axiom fo_not : FOFormula -> FOFormula.
Axiom fo_and : FOFormula -> FOFormula -> FOFormula.
Axiom fo_or : FOFormula -> FOFormula -> FOFormula.
Axiom fo_impl : FOFormula -> FOFormula -> FOFormula.
Axiom fo_iff : FOFormula -> FOFormula -> FOFormula.
Axiom fo_forall : nat -> FOFormula -> FOFormula.
Axiom fo_exists : nat -> FOFormula -> FOFormula.
(** * Pretty printer for FOL *)
Declare Custom Entry FOL.
Notation "[ e ]" := e (e custom FOL at level 0).
Notation "( x )" := x (in custom FOL, x at level 2).
Notation "x" := x (in custom FOL at level 0, x ident).
Notation "⊥" := fo_bot
(in custom FOL at level 0).
Notation "⊤" := fo_top
(in custom FOL at level 0).
Notation "¬ A" := (fo_not A)
(in custom FOL at level 35,
right associativity, format "'¬' A").
Infix "∧" := fo_and
(in custom FOL at level 40,
left associativity).
Infix "∨" := fo_or
(in custom FOL at level 50,
left associativity).
Infix "→" := fo_impl
(in custom FOL at level 99,
right associativity).
Infix "↔" := fo_iff
(in custom FOL at level 95,
right associativity).
Notation "∀ x A" := (fo_forall x A)
(in custom FOL at level 120,
left associativity).
Notation "∃ x A" := (fo_exists x A)
(in custom FOL at level 120,
left associativity).
(* Print fo_sub. *)
Section Check.
Context (A B : FOFormula) (x : nat).
Goal Type.
pose [ ¬(¬¬¬¬ A ∧ B) → A ∨ B ∧ A ↔ ∀ x A ].
pose [A ∨ A].
Admitted.
Check [A ∨ A].
End Check.
```

Maybe separate, but should the quantifiers use x ident?

Also does the not unary notation need associativity and a format?

Maybe did you solve the problem by the time. You need to use `global`

instead of `ident`

for atoms (in `Notation "x" := x (in custom FOL at level 0, x ident).`

). As it is, the name `ident`

is for variables bound locally or in the goal context, but not for section variables.

- @Paolo Giarrusso's remark on quantifiers.

Last updated: Jan 29 2023 at 06:02 UTC