2

I would like to typeset the following sequent: A | Γ ⊢ B. I have tried,

\documentclass{article}
\begin{document}
$A \mid \Gamma \vdash B$
\end{document}

but \mid has a much greater height that \vdash. I could measure the height of the turnstile symbol and draw a matching vertical rule, but then I could not copy-paste formulas from the output PDF (and I am not sure the thickness and corner rounding would match).

I am open to the idea of using something else than \vdash (for example a command from the turnstile package) as long as there is a matching vertical bar (you may call it \vnodash).

2 Answers 2

2

You could scale \mid so that it

  1. has the same height as \vdash, and
  2. sits on the baseline like \vdash.

The butts are not as rounded as in \vdash, but it shouldn't be a big problem in print.

\documentclass{article}
\usepackage{amsmath}
\usepackage{graphicx}

\makeatletter
\NewDocumentCommand{\vmid}{}{\mathrel{\mathpalette\vmid@\relax}}
\newcommand{\vmid@}[2]{%
  \begingroup
  \sbox\z@{$#1\vdash$}%
  \resizebox{\width}{\ht\z@}{\raisebox{\depth}{$\m@th#1|$}}%
  \endgroup
}
\makeatother

\begin{document}

$A \vmid \Gamma \vdash B$

\end{document}

enter image description here

1
  • I think that's the best solution, thank you.
    – user316110
    Apr 15 at 16:26
2

You can create \vnodedash with an assemblage of \mid and -

\NewDocumentCommand{\vnodedash}{}{\mid\mkern -4.35mu\relax\mathrel{-}}

Example

\documentclass{article}

\NewDocumentCommand{\vnodedash}{}{\mid\mkern -4.35mu\relax\mathrel{-}}

\begin{document}
$A \mid \Gamma \vdash B$

$A \mid \Gamma \vnodedash B$

\end{document}

\vnodedash example

2
  • Thank you for your answer, where does the number -4.35mu come from?
    – user316110
    Apr 15 at 12:47
  • @richardIII Trials and errors. You need maybe to adapt this value with different font size (with 12pt the dash is shifted too far to the left). It also not perfect in \scripscripstyle (try $\scriptscriptstyle A \mid \Gamma \vnodedash B$).
    – jlab
    Apr 15 at 12:54

You must log in to answer this question.