Stream: Coq users

Topic: Notation for unpacking a value


view this post on Zulip 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.)

view this post on Zulip 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.

view this post on Zulip Anton Golov (they/them) (Dec 21 2022 at 13:24):

Ah, thank you! :D


Last updated: Jun 18 2024 at 09:02 UTC