AlgebraicJulia/Catlab.jl

LaTeX pretty-printing of GATs

Open

#243 ouverte le 24 août 2020

Voir sur GitHub
 (1 commentaire) (0 réactions) (1 assigné)Julia (68 forks)batch import
GATsenhancementgood first issue

Métriques du dépôt

Stars
 (706 stars)
Métriques de merge PR
 (Aucune PR mergée en 30 j)

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.

Guide contributeur

Direction de recherche
Examinez la sortie LaTeX existante dans Catlab.jl pour des constructions similaires (par exemple, les théories). Étudiez la notation pour les GATs dans l'article référencé. Implémentez d'abord la notation linéaire de style Cartmell en adaptant la syntaxe de la macro `@theory`, puis abordez la notation en arbre de déduction naturelle, éventuellement en utilisant des utilitaires de formatage d'arbre existants. Envisagez d'utiliser MathJax/KaTeX pour le rendu.
Stack technique
Aucun
Domaine
documentationtooling
Type d'issue
Fonctionnalité
DifficultéDifficulté estimée pour un nouveau contributeur, de 1 pour un très petit changement à 5 pour un travail expert.
3
Temps estiméFourchette de temps approximative pour investiguer, implémenter, tester et préparer une pull request.
1-2 jours
Statut d'activitéDisponibilité apparente de l'issue : fraîche, active, ancienne, bloquée ou en attente d'un mainteneur.
Ancienne
ClartéClarté avec laquelle l'issue explique le changement attendu, les critères d'acceptation et la prochaine étape.
Claire
Prérequis
Familiarity with JuliaUnderstanding of GATsKnowledge of LaTeX formatting
Accessibilité débutantScore de 1 à 100 estimant l'accessibilité de cette issue pour un premier contributeur.
35