The Coq mailing list

[Beta Ziliani <beta AT mpi-sws.org>]

Hi list,

We've been fighting this issue for way too long, and now it's time to ask the crowd. We like to override the notation for lists only when the list is the argument of certain definition. However, the notation is being pervasive to every list. Aren’t scopes intended for that? What is wrong with our understanding of scopes?

Many thanks,
Beta

Require Import Lists.List.
Import ListNotations.

Delimit Scope pattern_scope with pattern.
Delimit Scope patterns_scope with patterns.

Notation "a => b" := (a, b) (at level 201) : pattern_scope.
Notation "'with' p1 | .. | pn 'end'" :=
  ((cons p1%pattern (.. (cons pn%pattern nil) ..)))
    (at level 91, p1 at level 210, pn at level 210) : patterns_scope.

Definition mymatch (n:nat) (l : list (nat * nat)) := tt.
Arguments mymatch _ _%patterns.
Notation "'mmatch' n ls" := (mymatch n ls) (at level 0).

Close Scope patterns_scope.
Close Scope pattern_scope.

Definition amatch := mmatch 0 with 0 => 1 | 1 => 2 end.
Print amatch. (* Good: amatch = mmatch 0 (with 0 => 1| 1 => 2 end) *)

Definition alist := [0;1;2].
Print alist. (* Bad: alist = (with 0| 1| 2 end)%patterns *)

​