Skip to content

Commit

Permalink
don't run examples
Browse files Browse the repository at this point in the history
  • Loading branch information
olynch committed Oct 17, 2023
1 parent c950e76 commit 0647ff6
Show file tree
Hide file tree
Showing 2 changed files with 10 additions and 10 deletions.
18 changes: 9 additions & 9 deletions docs/src/concepts/symbolic_models.md
Original file line number Diff line number Diff line change
Expand Up @@ -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] ]
Expand All @@ -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))
```

Expand All @@ -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
Expand All @@ -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))
```

Expand All @@ -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())
Expand All @@ -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
Expand All @@ -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))
Expand Down
2 changes: 1 addition & 1 deletion docs/src/concepts/theories.md
Original file line number Diff line number Diff line change
Expand Up @@ -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:

Expand Down

0 comments on commit 0647ff6

Please sign in to comment.