☰

交叉引用推理规则

tag-icon • tag-icon cross-referencing logic
交叉引用推理规则

我正在使用mathpartirDidier Remy 的软件包来排版推理规则。我喜欢规则的视觉风格，但该软件包无法与标准交叉引用机制集成\label。\ref例如，在我排版肯定前件规则后：

\documentclass{article}
\usepackage{mathpartir}

\begin{document}
\begin{mathpar}
  \inferrule[ABC]{
    A \\
    A \Longrightarrow B
  }{
    B
  }{{\Longrightarrow}E}
\end{mathpar}
\end{document}

我希望以后能够使用来引用它\ref，并进行${\Longrightarrow}E$渲染。问题：

  1. 我可以用 来实现这个功能吗？如何实现？另外，关于和内部工作原理mathpartir的一般指示可能很有用 - 因为我没有太多的规则，所以我对 hacky 解决方案也很满意。\label\ref

  2. 您知道有任何可以实现此功能的替代软件包吗？

答案1

默认的交叉引用系统依赖于对交叉引用项进行编号。将\label{}当前适用的计数器的值.auz连同作为其参数给出的标签一起写入文件。\ref{}使用该标签检索计数器的值。计数器可以格式化为数字以外的其他内容，例如A，B而C不是1，，，但它仍然2是3一个数字。

由于推理规则没有编号，这显然不适用。此外，即使它们有编号，\ref{}也会返回计数器的值，而不是类似的东西-> E。

然而，该计划nameref是超链接包，扩展了标准交叉引用系统，以便可以.aux使用从文件中检索诸如部分之类的项目的名称\nameref{}。它通过重新定义\label{}将附加信息写入.aux文件来实现这一点。

我们可以使用这个框架进行重新定义，\inferrule以便后续\label{}将所需的信息写入文件.aux。默认情况下，根本-> E不是传递给的参数\inferrule- 它只是接下来的参数。所以我们需要重新定义\inferrule以接受一个额外的参数，最好是一个可选的参数。然后我们需要设置\@currentlabelname为这个参数的值（如果存在），这样它就\label{}知道要写入.aux文件的内容。

我已经习惯xparse处理重新定义。

我们首先保存当前的定义\inferrule。我们不需要这个，但用户可能需要。

\let\originferrule\inferrule

现在我们重写定义以接受最后一个可选参数。因此新语法将是\inferrule*[]{}{}[]而不是\inferrule*[]{}{}。

\DeclareDocumentCommand \inferrule { s O {} m m o }{%

我们是否需要带星号的表格？

  \IfBooleanTF{#1}%
  {%

我们所做的就是将参数 2、3 和 4 传递给相关的内部宏 - 带星号...

    \mpr@inferstar[#2]{#3}{#4}%
  }{%

或不 ...

    \mpr@inferrule[#2]{#3}{#4}%
  }%

现在我们测试用户是否使用了可选参数。如果没有，则无需执行任何操作。

  \IfValueT{#5}%
  {%

否则，我们增加一点空间，

    \quad

排版论点

    #5%

并将参数传递给另一个宏（我们马上定义）。

    \my@name@inferrule{#5}%
  }%

就是这样。

}

现在来看看最后一个宏。这只是设置\@currentlabelname为相关值，将其包装在以\ensuremath{}避免名称包含符号等时出现错误。

\NewDocumentCommand \my@name@inferrule { m }{%
  \def\@currentlabelname{\ensuremath{#1}}%
}

然后我们可以写

\begin{mathpar}
  \inferrule[Modus Ponens]{
    A \\
    A \Longrightarrow B
  }{
    B
  }[\Longrightarrow E]\label{infrule:mp}
\end{mathpar}
Applying \nameref{infrule:mp}, we see that \dots

生产

按名称引用推理规则

完整代码：

\documentclass{article}
\usepackage{mathpartir,xparse}
\usepackage{nameref}

\makeatletter
\let\originferrule\inferrule
\DeclareDocumentCommand \inferrule { s O {} m m o }{%
  \IfBooleanTF{#1}%
  {%
    \mpr@inferstar[#2]{#3}{#4}%
  }{%
    \mpr@inferrule[#2]{#3}{#4}%
  }%
  \IfValueT{#5}%
  {%
    \quad
    #5%
    \my@name@inferrule{#5}%
  }%
}
\NewDocumentCommand \my@name@inferrule { m }{%
  \def\@currentlabelname{\ensuremath{#1}}%
}
\makeatother

\begin{document}
\begin{mathpar}
  \inferrule[Modus Ponens]{
    A \\
    A \Longrightarrow B
  }{
    B
  }[\Longrightarrow E]\label{infrule:mp}
\end{mathpar}
Applying \nameref{infrule:mp}, we see that \dots
\end{document}

相关内容