From 0647ff6637e8be5347c756e60a8df3621205410d Mon Sep 17 00:00:00 2001 From: Owen Lynch Date: Mon, 16 Oct 2023 19:47:33 -0700 Subject: [PATCH] don't run examples --- docs/src/concepts/symbolic_models.md | 18 +++++++++--------- docs/src/concepts/theories.md | 2 +- 2 files changed, 10 insertions(+), 10 deletions(-) diff --git a/docs/src/concepts/symbolic_models.md b/docs/src/concepts/symbolic_models.md index 50785f14..d29bdd73 100644 --- a/docs/src/concepts/symbolic_models.md +++ b/docs/src/concepts/symbolic_models.md @@ -16,7 +16,7 @@ To get started, you can always call the `@symbolic_model` macro with an empty bo Below, we subtype from GATlab's abstract types `ObExpr` and `HomExpr` to enable LaTeX pretty-printing and other convenient features, but this is not required. -```@example category +```julia @symbolic_model CategoryExprs{ObExpr, HomExpr} ThCategory begin end A, B, C, D = [ Ob(CategoryExprs.Ob, X) for X in [:A, :B, :C, :D] ] @@ -27,7 +27,7 @@ compose(compose(f,g),h) The resulting symbolic expressions perform no simplification. For example, the associativity law is not satisfied: -```@example category +```julia compose(compose(f,g),h) == compose(f,compose(g,h)) ``` @@ -36,12 +36,12 @@ obey all the axioms of the theory. However, the user may supply logic in the body of the `@symbolic_model` macro to enforce the axioms or perform other kinds of simplification. Below, we use the -[`associate`](@ref) function provided by GATlab to convert the binary +`associate` function provided by GATlab to convert the binary expressions representing composition into $n$-ary expressions for any number $n$. The option `strict=true` tells GATlab to check that the domain and codomain objects are strictly equal and throw an error if they are not. -```@example category +```julia @symbolic_model SimplifyingCategoryExprs{ObExpr, HomExpr} ThCategory begin compose(f::Hom, g::Hom) = associate(new(f,g; strict=true)) end @@ -52,7 +52,7 @@ compose(compose(f,g),h) Now the associativity law *is* satisfied: -```@example category +```julia compose(compose(f,g),h) == compose(f,compose(g,h)) ``` @@ -73,11 +73,11 @@ determine which operations, if any, will be derived from others. In the case of the cartesian monoidal category, we could define a signature `CartesianCategory` by inheriting from the builtin theory `SymmetricMonoidalCategory`. -```@setup cartesian-monoidal-category +```julia using GATlab ``` -```@example cartesian-monoidal-category +```julia @signature ThCartesianCategory <: ThSymmetricMonoidalCategory begin mcopy(A::Ob)::(A → (A ⊗ A)) delete(A::Ob)::(A → munit()) @@ -90,7 +90,7 @@ nothing # hide We could then define the copying operation in terms of the pairing. -```@example cartesian-monoidal-category +```julia @symbolic_model CartesianCategoryExprsV1{ObExpr,HomExpr} ThCartesianCategory begin mcopy(A::Ob) = pair(id(A), id(A)) end @@ -101,7 +101,7 @@ mcopy(A) Alternatively, we could define the pairing and projections in terms of the copying and deleting operations. -```@example cartesian-monoidal-category +```julia @symbolic_model CartesianCategoryExprsV2{ObExpr,HomExpr} ThCartesianCategory begin pair(f::Hom, g::Hom) = compose(mcopy(dom(f)), otimes(f,g)) proj1(A::Ob, B::Ob) = otimes(id(A), delete(B)) diff --git a/docs/src/concepts/theories.md b/docs/src/concepts/theories.md index ffcb41d1..3dbd9c08 100644 --- a/docs/src/concepts/theories.md +++ b/docs/src/concepts/theories.md @@ -59,7 +59,7 @@ algebra, thus, providing a perfect opportunity for computer algebra systems. GATlab implements a version of the GAT formalism on top of Julia's type system, taking advantage of Julia macros to provide a pleasant syntax. GATs are defined -using the [`@theory`](@ref) macro. +using the `@theory` macro. For example, the theory of categories could be defined by: