There are tutorials that have out of date code such as the following GATlab code in the tutorial on preorders
@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
@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
There are tutorials that have out of date code such as the following GATlab code in the tutorial on preorders
which should be
This and related code blocks should be brought up to date