In my code I've often run into expressions like `∃ y, x = f y ∧ P`

, where `P`

depends on `y`

. I was hoping to make a notation for this, and I tried

```
Notation "'Unpack' x 'as' f y , P" :=
(∃ y, x = f y ∧ P)
(at level 200, y binder).
```

However, while the notation definition is accepted, trying to use the notation fails:

```
Definition g y := y + 1.
Theorem test : Unpack 5 as g y, y = 4.
```

gives `Syntax error: [one_open_binder] expected after [term level 200] (in [binder_constr]).`

I think this is a problem with delimiting `f`

from `y`

, but is there any way to solve it? I'm fine with `f`

having to be a constructor, if that helps.

(This is a somewhat simplified example, in my code I'm working with separation logic, but I think the idea is the same.)

```
Notation "'Unpack' x 'as' f y , P" :=
(exists y, x = f y /\ P)
(at level 200, f global).
Definition g y := y + 1.
Theorem test : Unpack 5 as g y, y = 4.
```

Ah, thank you! :D

Last updated: Jun 18 2024 at 09:02 UTC