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...

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