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: Oct 13 2024 at 01:02 UTC