search

AlgebraicJulia / GATlab.jl

GATlab: a computer algebra system based on generalized algebraic theories (GATs)
https://algebraicjulia.github.io/GATlab.jl/
MIT License
21 stars 2 forks source link

Docstrings for GAT modules #139

Closed olynch closed 4 months ago

olynch commented 5 months ago

When you declare a new GAT with @theory, the produced module should have a good docstring.

jpfairbanks commented 5 months ago

Do we want to capture any structured metadata about the GAT in this issue? For example a link to a paper or something? We can use this to provide a database of GATs in the docs.

jpfairbanks commented 5 months ago

Current behavior

help?> GATlab.StdTheories.ThCMonoid
  No docstring or readme file found for module GATlab.Stdlib.StdTheories.ThCMonoid.

  Exported names
  ≡≡≡≡≡≡≡≡≡≡≡≡≡≡

  default, e, ⋅

that docstring should include:

julia> GATlab.StdTheories.ThCMonoid.Meta.theory
GAT(ThCMonoid):
  default::TYPE ⊣ []
  (x ⋅ y)::default ⊣ [x::default, y::default]
  ((x ⋅ y) ⋅ z == x ⋅ (y ⋅ z)) ⊣ [x::default, y::default, z::default]
  e()::default ⊣ []
  (e() ⋅ x == x) ⊣ [x::default]
  (x ⋅ e() == x) ⊣ [x::default]
  (a ⋅ b == b ⋅ a) ⊣ [a::default, b::default]