GATsenhancementgood first issue
仓库指标
- Star
- (706 star)
- PR 合并指标
- (30 天内没有已合并 PR)
描述
Pretty-print GATs as LaTeX in both of the following styles:
-
Cartmell-style linear notation
-
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.