Is there some kind of trick to make the syntax _⊢_:_ \_ \vdash \_ : \_ _⊢_:_ non-ambiguous? As it is it overlaps with the syntax ::: for ∈\in∈.
I usually just do no_notation Set.member ("(_/ : _)" [51, 51] 50) because AFAIK noone uses it anyways
no_notation Set.member ("(_/ : _)" [51, 51] 50)
Last updated: Feb 01 2025 at 20:19 UTC