代码之家  ›  专栏  ›  技术社区  ›  Cactus

从LaTeX输出隐藏行的部分

  •  1
  • Cactus  · 技术社区  · 8 年前

    有没有办法从LaTeX输出中隐藏部分行?

    对于整条线路,这项工作:

    \begin{code}
    foo : Tm Γ t
    \end{code}
    \begin{code}[hide]
    foo = someHiddenDefinitionOfFoo
    \end{code}
    

    但是,如果我想隐藏行的某些部分,例如类型签名的某些部分,该怎么办?例如,假设我有Agda签名:

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

    但我希望在乳胶输出中是这样的:

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

    这可能吗?

    2 回复  |  直到 8 年前
        1
  •  1
  •   gallais    8 年前

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

    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)
    
        2
  •  -3
  •   Benjamin Barrois    8 年前

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

    \begin{comment}
        Something not taken into account
    \end{comment}
    
    推荐文章