AlgebraicJulia/Catlab.jl

LaTeX pretty-printing of GATs

Open

#243 aperta il 24 ago 2020

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

Metriche repository

Star
 (706 star)
Metriche merge PR
 (Nessuna PR mergiata 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
Esamina l'output LaTeX esistente in Catlab.jl per costrutti simili (ad esempio, teorie). Studia la notazione per GATs nel documento di riferimento. Implementa prima la notazione lineare in stile Cartmell adattando la sintassi della macro `@theory`, quindi affronta la notazione ad albero di deduzione naturale, eventualmente utilizzando utility esistenti per la formattazione ad albero. Valuta l'utilizzo di MathJax/KaTeX per il rendering.
Tech stack
Nessuno
Dominio
documentationtooling
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.
Datata
ChiarezzaQuanto chiaramente la issue descrive problema, scope e risultato atteso.
Chiara
Prerequisiti
Familiarity with JuliaUnderstanding of GATsKnowledge of LaTeX formatting
Adatta ai principiantiQuanto la issue è adatta a contributor alla prima esperienza.
35