排版霍尔三元组 - 填充

Question

我正在尝试排版霍尔三元组，它用于推理程序的正确性。在我引用的文本中，它们看起来像这样：

我知道该stmaryrd包中包含相关命令，因此我尝试了如下操作：

\usepackage{stmaryrd}
\usepackage{mathtools}
\DeclarePairedDelimiter\Hoare{\llparenthesis}{\rrparenthesis}
% ...
\[
    \Hoare*{x > 0} P \Hoare*{y \cdot y < x}
\]

不幸的是，这给了我一个Missing delimiter (. inserted). \Hoare*{x > 0}错误。如果我从命令中删除星号，它会编译，但空格看起来离开：

注意括号与前置条件和后置条件的内容有多接近。我应该如何改进这一点？

Answer 1

符号\llparenthesis和\rrparenthesis不是“增长分隔符”，并且仅在标准尺寸下可用。

我建议采用不同的语法，以应对中间术语的间距：

\documentclass{article}
\usepackage{stmaryrd}

\newcommand\Hoaretriple[3]{%
  \llparenthesis\,#1\,\rrparenthesis
  \mathrel{#2}\nolinebreak 
  \llparenthesis\,#3\,\rrparenthesis
}

\begin{document}

\[
\Hoaretriple{x > 0}{ P }{y \cdot y < x}
\]

\end{document}

Answer 2

您可以通过插入手动修复间距一些命令可以。可以\Hoare像我一样在定义中插入空格，也可以直接在公式中插入空格。

\documentclass{article}
\usepackage{stmaryrd}
\usepackage{mathtools}
\DeclarePairedDelimiter\Hoare{\,\llparenthesis\,}{\,\rrparenthesis\,}
\begin{document}
\[
    \Hoare{x > 0} P \Hoare{y \cdot y < x}
\]
\end{document}