AlgebraicJulia/Catlab.jl

LaTeX pretty-printing of GATs

Open

#243 建立於 2020年8月24日

在 GitHub 查看
 (1 留言) (0 反應) (1 負責人)Julia (706 star) (68 fork)batch import
GATsenhancementgood first issue

描述

Pretty-print GATs as LaTeX in both of the following styles:

  1. Cartmell-style linear notation

  2. natural-deduction-style tree notation

The examples above depict the theory of monoids and are taken from Sterling's paper Algebraic type theory and universe hierarchies.

The first style is similar to the syntax of our @theory macro and should be easily ported to MathJax/KaTeX, while the second style is harder to typeset but beloved by type theorists.

貢獻者指南

技術棧
無
領域
documentationtooling
議題類型
feature
難度面向新貢獻者的預計實作難度，1 表示很小改動，5 表示專家級工作。
3
預計時間有經驗貢獻者完成調查、實作、測試並準備 pull request 的粗略時間範圍。
1-2 days
活動狀態議題目前的可參與程度：新鮮、活躍、陳舊、阻塞或等待維護者輸入。
stale
清晰度議題是否清楚說明預期改動、驗收標準和下一步。
clear
前置要求
Familiarity with JuliaUnderstanding of GATsKnowledge of LaTeX formatting
新手友善度1-100 的估計分數，表示該議題對首次貢獻者的友善程度。
35
研究方向
Examine existing LaTeX output in Catlab.jl for similar constructs (e.g., theories). Study the referenced paper's notation for GATs. Implement first the Cartmell style linear notation by adapting the `@theory` macro's syntax, then tackle the natural deduction tree notation, possibly using existing tree formatting utilities. Consider leveraging MathJax/KaTeX for rendering.