TURNSTILE-INDENT-AUTO : FLAGTURNSTILE-INDENT-AUTO is a flag or parameter.
Decides how turnstiles are printed in proofs. This flag works in
all styles other than TEX; in particular, it works in XTERM, GENERIC,
SCRIBE and SLIDES styles. There are four possible settings:
FIX : put the turnstile in the column indicated by TURNSTYLE-INDENT
(or SLIDES-TURNSTYLE-INDENT, in style SLIDES).
MIN : print the turnstile as far to the left as possible while still having
it in the same column on every line. (If this puts it off the right
margin, then this will default to the same behaviour as FIX.)
COMPRESS : similar to VARY, but also removes spaces at other points in the
proof (e.g. around dots, and between line numbers and hypotheses).
VARY : print the turnstile one space after the hypotheses in each line
(so it will move from line to line).
TURNSTILE-INDENT-AUTO takes values of type INDENTATION.
It belongs to subjects OTL-VARS PRINTING .
Its default value is MIN
Its current value is MIN.
TPS documentation homepage