☰

如何在单个块中混合 lhs2TeX 代码和规范行？

tag-icon • tag-icon spacing lhs2tex
如何在单个块中混合 lhs2TeX 代码和规范行？

假设我有一个不完整的代码块，例如：

\documentclass{article}
%include polycode.fmt
\begin{document}
\begin{code}
somefunction :: a -> a
\end{code}
\begin{spec}
somefunction x = undefined
\end{spec}
\end{document}

它应该表达一项正在进行的工作，因为somefunction它只是在稍后定义，所以我想从 ghc 隐藏这个不完整的定义，但我想重用类型签名。不幸的是，在这个设置中，两行之间有一个垂直空格。一种解决方法是重写文档主体，如下所示：

\begin{spec}
somefunction :: a -> a
somefunction x = undefined
\end{spec}
%if False
\begin{code}
somefunction :: a -> a
\end{code}
%endif

这样做的缺点是重复性较强，因此容易引入错误。

插入的空间似乎与\belowdisplayskip+ \baselineskip+有关\abovedisplayskip，因此可以\vspace在前一个定义中添加负数。

空间真的是上述内容的总和吗？对于粘合code和spec环境，建议采用哪种解决方案？

答案1

在这种情况下，推荐的解决方案如下：

\documentclass{article}
%include polycode.fmt
\begin{document}
%format somefunction0 = somefunction

> somefunction :: a -> a
> somefunction0 x = undefined

Much later:

> somefunction = id

\end{document}

这样做的好处是，即使是初步代码在通过 GHC 运行时仍会进行类型检查。（使用>Instead ofcode和<Instead ofspec并不相关，但由于您抱怨噪音，我认为可能值得指出。这种风格的代码/规范块周围的空行是必需的。）

答案2

基于 kosmikus 解决方案，让我给出一个 Agda 的扩展解决方案，避免重复类型签名。（对于评论来说有点太长了。）它需要更多的设置代码：

\documentclass{article}
%include agda.fmt
\begin{document}
%if False
\begin{code}
open import Reflection
termoftype : Type → Term
termoftype (el s t) = t
\end{code}
%endif

然后我们可以重用 kosmikus 技术：

%format somefunction0 = somefunction
\begin{code}
somefunction0 : {a : Set} → a → a
somefunction0 x = ?
\end{code}

我们不需要再次编写（可能很长的）类型签名，而是可以通过反射来获取它：

Much later:
%if False
\begin{code}
somefunction : unquote (termoftype (type (quote somefunction0)))
\end{code}
%endif
\begin{code}
somefunction = id
\end{code}
\end{document}

相关内容