The Coq mailing list

[Jason Gross <jasongross9 AT gmail.com>]

As far as I'm aware, overloading builtin notations (or tactic notations) with an identity notation is the standard way to keep them accessible after overloading them.  I think the only even-slightly-sketchy thing is that your `%type` is, I think, both unnecessary and stronger than the existing built-in notation.  (I think you also want to say `y` binder, though?  I'm not sure if it's needed.)  See https://github.com/coq/coq/issues/12157 for some details about the two different kinds of scope stacks.

On Tue, Apr 21, 2020 at 11:34 PM Gregory Malecha <gmalecha AT gmail.com> wrote:

Hello --

I'm working on notation for an embedded logic and I'm wondering how sketchy the following is with respect to any special handling that Coq might do when parsing "forall".

Notation "'forall' x .. y , P" :=
  (forall x, .. (forall y, P%type) ..) (at level 200, x binder, right associativity, only parsing) : type_scope.

Notation "'forall' x .. y , P" :=
  (bi_forall (fun x => .. (bi_forall (fun y => P%I)) ..)) (at level 200, x binder, right associativity, only parsing) : bi_scope.

Without the first rule, I seem to completely loose access to Coq's primitive forall.

I tried the following alternative where I don't put forall in single quotes:

Notation "forall x .. y , P" :=
  (bi_forall (fun x => .. (bi_forall (fun y => P%I)) ..)) (at level 200, x binder, right associativity, only parsing) : bi_scope.

But this doesn't seem to work, it either silently ignores the rule, or it ignores the %I annotation on P and attempts to parse the body using type scope.

Thanks!

--

gregory malecha

gmalecha.github.io