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.
Syntax error: [one_open_binder] expected after [term level 200] (in [binder_constr]).
I think this is a problem with delimiting
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 04 2023 at 20:01 UTC