# Pattern matching notation for monadic binds

This gets rid of the old hack to have specific notations for pairs up to a fixed arity, and moreover allows to do fancy things like:

```
Record test := Test { t1 : nat; t2 : nat }.
Definition foo (x : option test) : option nat :=
''(Test a1 a2) ← x;
Some a1.
```

There are some problems, however:

- It conflicts with Coq's notation
`' x`

for`Zpos x`

. Fortunately, the breakage is in the right direction: the proposed monadic notation breaks Coq's`' x`

. Furthermore, I believe said notation should be removed from Coq, see https://github.com/coq/coq/pull/6155 - It breaks backwards compatibility. Since Coq only allows to use binders in recursive notations, the notation must start with at least one symbol, for which I picked
`'`

. As such, this means we need a double`'`

.

Edited by Robbert Krebbers