Is there a notation for "$x$ is not typed $y$"? The context is
$x : z \:\: \vdash \:\: x$ is not typed $y$,
with $z$ and $y$ suitably defined. The obvious but awkward (and even ambiguous) thing I thought about is
$x : z \:\: \vdash \:\: ¬$t$(x, y)$,
where t is a predicate "is typed". The next-to-obvious thing is
$x : z \:\: \vdash \:\: x$
:$y$,
which is obviously ad hoc and in this case just doesn't work (minimally, I'd need a diagonal strikeout)
I would eventually use the notation in Latex, but this isn't a Latex question, as it's about a notation (and not about how to get a diagonal strikeout in Latex, which I know how to do)