GATsenhancementgood first issue
Repository metrics
- Stars
- (706 stars)
- PR merge metrics
- (30d に merged 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.