\documentclass[fleqn,leqno]{article}
\usepackage{hypertlabook}
\makeindex
\file{if-vs-if}
\pdftitle{IF Versus if}
\begin{popup}
{\large \textsc{if} Versus \textbf{if}}

\medskip

  \ctindex{1}{if versus if@\icmd{textsc}{if} versus \icmd{textbf}{if}}{}%
Don't confuse \textsc{if} (typed \verb|IF|), which begins a \tlaplus\
expression, with \textbf{if} (typed \verb|if|), which begins a PlusCal
statement.  The keyword \textbf{if} can occur only in a PlusCal
algorithm, which appears in a comment within the module.  The keyword
\textsc{if} can appear in a \tlaplus\ expression, so it can appear in
either a \tlaplus\ specification or in an expression in a PlusCal
algorithm.  (Any \tlaplus\ expression can be used as an expression in
a PlusCal algorithm.)
\end{popup}
\makepopup