AlgebraicJulia/Catlab.jl

LaTeX pretty-printing of GATs

Open

#243 opened on Aug 24, 2020

View on GitHubContributor guide
 (1 comment) (0 reactions) (1 assignee)Julia (68 forks)batch import
GATsenhancementgood first issue

Repository metrics

Stars
 (706 stars)
PR merge metrics
 (Avg merge 17d 19h) (2 merged PRs in 30d)

Description

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.

Contributor guide

Research direction
Inspect the existing @theory macro and the LaTeX pretty printing infrastructure in Catlab.jl, then implement the two styles: Cartmell style linear notation and natural deduction style tree notation. Follow the examples from Sterling's paper.
Tech stack
julia
Domain
documentation
Issue type
Feature
DifficultyEstimated implementation difficulty for a new contributor, from 1 for very small changes to 5 for expert-level work.
3
Estimated timeA rough time range for an experienced contributor to investigate, implement, test, and prepare a pull request.
1-2 days
Activity statusHow available the issue appears right now: fresh, active, stale, blocked, or waiting on maintainer input.
Active
ClarityHow clearly the issue explains the expected change, acceptance criteria, and next step.
Clear
Prerequisites
Julia
Newbie friendlinessA 1-100 score estimating how approachable this issue is for first-time contributors.
70