AlgebraicJulia/Catlab.jl

LaTeX pretty-printing of GATs

Aperta

#243 aperta il 24 ago 2020

Vedi su GitHubGuida contributor
 (1 commento) (0 reazioni) (1 assegnatario)Julia (68 fork)batch import
GATsenhancementgood first issue

Metriche repository

Star
 (706 stelle)
Metriche merge PR
 (Merge medio 17g 19h) (2 PR mergiate in 30 g)

Descrizione

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.

Guida contributor

Direzione di ricerca
Ispeziona la macro @theory esistente e l'infrastruttura di pretty printing LaTeX in Catlab.jl, quindi implementa due stili: la notazione lineare in stile Cartmell e la notazione ad albero in stile deduzione naturale. Segui gli esempi del paper di Sterling.
Tech stack
julia
Dominio
documentation
Tipo issue
Funzionalità
DifficoltàQuanto dovrebbe essere impegnativa per un nuovo contributor.
3
Tempo stimatoTempo stimato per completare e verificare uno scope piccolo.
1-2 giorni
Stato attivitàQuanto è probabile che la issue sia ancora attiva e reviewable.
Attiva
ChiarezzaQuanto chiaramente la issue descrive problema, scope e risultato atteso.
Chiara
Prerequisiti
Julia
Adatta ai principiantiQuanto la issue è adatta a contributor alla prima esperienza.
70