## Stream: Coq users

### Topic: notations

#### Jason Gross (Jun 06 2020 at 03:53):

Is there a way to get this to work without the parentheses? (cc @Hugo Herbelin )

``````Notation "'WITH' ( x1 : t1 ) , x2t2 , .. , xntn  'PRE'  [ ] P 'POST' [ ] Q" :=
(((fun x1 : t1 => (fun x2t2 => .. (fun xntn => (pair .. (pair x1 x2t2) .. xntn)) .. )),
(fun x1 : t1 => (fun x2t2 => .. (fun xntn => P) .. )),
(fun x1 : t1 => (fun x2t2 => .. (fun xntn => Q) .. ))))
(at level 200, x1 at level 0, x2t2 closed binder, xntn closed binder, P at level 100, Q at level 100).

Check WITH (x : nat) , (y : nat) , (z : unit) PRE [] (x, y, z) POST [] (z, y, x).
``````

That is, I want

``````Check WITH x : nat , y : nat , z : unit PRE [] (x, y, z) POST [] (z, y, x).
``````

to work. I can do

``````Notation "'WITH' x1 : t1 , x2t2 , .. , xntn  'PRE'  [ ] P 'POST' [ ] Q" :=
(((fun x1 : t1 => (fun x2t2 => .. (fun xntn => (pair .. (pair x1 x2t2) .. xntn)) .. )),
(fun x1 : t1 => (fun x2t2 => .. (fun xntn => P) .. )),
(fun x1 : t1 => (fun x2t2 => .. (fun xntn => Q) .. ))))
(at level 200, x1 at level 0, x2t2 closed binder, xntn closed binder, P at level 100, Q at level 100).
``````

but I can't figure out a replacement for "closed binder" that removes the parentheses (I'm willing to have it be one that requires the `:` to always be present). If I remove `closed`, then I get the error message `Error: as x2t2 is a non-closed binder, no such "," is allowed to occur.` If I replace `closed binder` with `at level 0`, I get `Anomaly "Inconsistent substitution of recursive notation."` on the `Check` (reported at https://github.com/coq/coq/issues/12467). If I replace `x1t1` with `x1 : t1` and `xntn` with `xn : tn`, I get `Cannot find where the recursive pattern starts.`. Not sure what else to try here...

#### Hugo Herbelin (Jun 09 2020 at 21:27):

If we remove the restriction on closed binders (and allow it even in the presence of a `,`), you'd be allowed to write things like `Check WITH (x : nat) , y y' , (z : unit) PRE [] (x, y, z) POST [] (z, y, x).` where `y` and `y'` are not separated by a `,`. Is this what you'd really want?

I suspect that you'd like some `unary binder` incantation, which typically tells to allow any of `x`, `x:T`, `x:=c`, `{x : T}`, `[x : T]` as a binder. This is not implemented though...

Last updated: Feb 08 2023 at 23:03 UTC