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: Dec 21 2024 at 16:20 UTC