((∑[T𝒰]∏A∈T]A≃1
@suhorng
Sat, Aug 12, 2023 5:27 AM
好像是可以用 minted 配合 pygmentize 直接把 Agda 檔案的片段加入到 LaTeX 中
((∑[T𝒰]∏A∈T]A≃1
@suhorng
Sat, Aug 12, 2023 5:29 AM
https://arxiv.org/... 有 frozen cache 這種直接把 cache 定版的選項呀
((∑[T𝒰]∏A∈T]A≃1
@suhorng
Sat, Aug 12, 2023 5:34 AM
https://people.csail.mit.edu/...
XOO
@xcycl
Sat, Aug 12, 2023 6:59 AM
lhs2tex 呢？
((∑[T𝒰]∏A∈T]A≃1
@suhorng
Sat, Aug 12, 2023 7:03 AM
還沒研究懂怎麼配合 lhs2tex
我想要做到類是 \inputAgdaCodeAtLines{FILE}{NN}{MM} 這樣, 不是用 literate Agda 寫
XOO
@xcycl
Tue, Sep 12, 2023 3:36 AM
lhs2tex 不用 literate Agda，他可以處理 \begin{code} … \end{code} 裡頭的 Agda code
載入新的回覆