Stream: Coq users

Topic: Custom notation not printing


view this post on Zulip Ali Caglayan (Oct 07 2021 at 17:06):

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.

view this post on Zulip Paolo Giarrusso (Oct 07 2021 at 21:53):

Maybe separate, but should the quantifiers use x ident?

view this post on Zulip Paolo Giarrusso (Oct 07 2021 at 21:54):

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

view this post on Zulip Hugo Herbelin (Oct 22 2021 at 13:11):

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.

view this post on Zulip Hugo Herbelin (Oct 22 2021 at 13:13):


Last updated: Jan 29 2023 at 06:02 UTC