从LaTeX输出隐藏行的部分

做这类事情最可靠的方法是 要隐藏的参数的匿名模块:

sub-⊢*⊇ : ∀ {Γ Δ Θ t} (σ : Γ ⊢* Δ) (Δ⊇Θ : Δ ⊇ Θ) (e : Tm Θ t) →
  sub (σ ⊢*⊇ Δ⊇Θ) e ≡ sub σ (ren Δ⊇Θ e)

因此成为

module _ {Γ Δ Θ t} where

 sub-⊢*⊇ : (σ : Γ ⊢* Δ) (Δ⊇Θ : Δ ⊇ Θ) (e : Tm Θ t) →
   sub (σ ⊢*⊇ Δ⊇Θ) e ≡ sub σ (ren Δ⊇Θ e)

如果你愿意使用非常基本的 sed 对LaTeX文件进行后处理以擦除simple的脚本 {var} 您应该能够通过以下方式实现预期目标:

module _ {Γ Δ Θ t} where

 sub-⊢*⊇ : ∀ σ Δ⊇Θ e → sub {Γ} (σ ⊢*⊇ Δ⊇Θ) e ≡ sub σ (ren {Δ} {Θ} Δ⊇Θ e)

这个 verbatim 软件包提供了 comment 环境

\begin{comment}
    Something not taken into account
\end{comment}