Stream: Coq users

Topic: Notation for unpacking a value

Anton Golov (they/them) (Dec 21 2022 at 13:05):

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

Li-yao (Dec 21 2022 at 13:22):

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

Anton Golov (they/them) (Dec 21 2022 at 13:24):

Ah, thank you! :D

Last updated: Jun 18 2024 at 09:02 UTC