AlgebraicJulia / AlgebraicJulia/Catlab.jl

Out of date GATlab examples

未關閉
#977 0 則留言 0 個 reaction 已指派 0 人 在 GitHub 檢視
docs
主要語言
Julia
星號
724
分支
73
PR 合併指標
30 天內沒有已合併 PR

描述

There are tutorials that have out of date code such as the following GATlab code in the tutorial on preorders

```julia
@theory Preorder{El,Leq} begin
El::TYPE
Leq(lhs::El, rhs::El)::TYPE
@op (≤) := Leq

# Preorder axioms are lifted to term constructors in the GAT.
reflexive(A::El)::(A≤A) # ∀ A there is a term reflexive(A) which implies A≤A
transitive(f::(A≤B), g::(B≤C))::(A≤C) ⊣ (A::El, B::El, C::El)

# Axioms of the GAT are equivalences on terms or simplification rules in the logic
f == g ⊣ (A::El, B::El, f::(A≤B), g::(A≤B))
# Read as (f⟹ A≤B ∧ g⟹ A≤B) ⟹ f ≡ g
end
```

which should be

```julia
@theory Preorder begin
El::TYPE
Leq(lhs::El, rhs::El)::TYPE
@op (≤) := Leq
reflexive(A::El)::(A≤A)
transitive(f::Leq(A,B), g::Leq(B,C))::Leq(A,C) ⊣ [A::El, B::El, C::El]
f == g ⊣ [A::El, B::El, f::Leq(A,B), g::Leq(A,B)]
end
```

This and related code blocks should be brought up to date

貢獻指南

開啟貢獻指南

評估

這個 Issue 還沒有評估資料。

把新 issue 寄到你的電子郵件信箱

精選適合新手參與的 GitHub issue 摘要。