Stream: Coq users

Topic: ✔ Notation in section

James Wood (Aug 04 2022 at 09:28):

I've defined a notation within a section (see below). I want to use the notation both later in that section and outside the section. Is there a way of making that possible without repeating the Notation declaration?

Section foo.
  Context {A : Type}.

  Fixpoint myapp (xs ys : list A) : list A :=
    match xs with
    | nil => ys
    | cons x xs => cons x (myapp xs ys)
    end.

  Notation "xs +++ ys" := (myapp xs ys) (at level 60, right associativity).

  Definition app3 (xs ys zs : list A) : list A := xs +++ ys +++ zs.

End foo.

Fail Check cons 1 nil +++ cons 2 nil.

Gaëtan Gilbert (Aug 04 2022 at 09:42):

there is not

Notification Bot (Aug 04 2022 at 10:53):

James Wood has marked this topic as resolved.

Last updated: Oct 13 2024 at 01:02 UTC