📄️ AddCommGroup
AddCommGroup represents an Abelian group. It's a commutative, additive group.
📄️ AddCommMonoid
AddCommMonoid represents a commutative, additive monoid.
📄️ AddCommSemigroup
Extending the additive semigroup with commutativity.
📄️ AddGroup
An additive group is an additive monoid that also has inverses.
📄️ AddLeftOrderedGroup
A left-ordered group is a group with a left-invariant order.
📄️ AddMonoid
An additive monoid is an additive semigroup with an identity element.
📄️ AddOrderedGroup
An ordered group has both left and right invariance.
📄️ AddSemigroup
An additive semigroup is associative, and that's about it.
📄️ Color
A simple enumeration type used as an example of a metric space with the discrete metric.
📄️ CommGroup
CommGroup represents an Abelian group. It's a commutative, multiplicative group.
📄️ CommMonoid
CommMonoid represents a commutative, multiplicative monoid.
📄️ CommRing
A commutative ring is a ring where multiplication is also commutative.
📄️ CommSemigroup
Extending the multiplicative semigroup with commutativity.
📄️ Complex
Complex numbers consist of a real part and an imaginary part.
📄️ Field
A field is a commutative ring with multiplicative inverses for all non-zero elements.
📄️ FiniteGroup
A group is finite if its elements can be placed in a (finite) list
📄️ FiniteSet
A finite set is a Set bundled with a finiteness proof.
📄️ FiniteSubgroup
A finite subgroup of a finite group.
📄️ Group
A group is a monoid that also has inverses.
📄️ GroupHom
A group homomorphism that preserves the group structure.
📄️ Int
The Int type represents integers.
📄️ LeftOrderedGroup
A left-ordered group is a group with a left-invariant order.
📄️ LinearOrder
A linear order (total order) is a partial order where all elements are comparable.
📄️ List
A generic list data structure that can hold elements of any type.
📄️ MetricSpace
A metric space is a set equipped with a distance function that satisfies specific axioms.
📄️ Monoid
A multiplicative monoid is a multiplicative semigroup with an identity element.
📄️ Multiset
A multiset (bag) that can contain multiple copies of the same element.
📄️ Nat
Natural numbers, the soul of arithmetic.
📄️ Option
Optional values that can either contain a value of type T or be empty.
📄️ OrderedField
A field with a total order compatible with the field operations.
📄️ OrderedGroup
An ordered group has both left and right invariance of the order under multiplication.
📄️ Pair
An ordered pair of two values, possibly of different types.
📄️ PartialOrder
A partial order is a relation that is reflexive, transitive, and antisymmetric.
📄️ Rat
Rational numbers represented as fractions in reduced form.
📄️ Real
Real numbers are defined by a Dedekind cut. Specifically, using the gt_rat function which
📄️ Ring
A ring is a structure with two operations (addition and multiplication) where addition forms an abelian group,
📄️ Semigroup
The default semigroup uses the multiplication operator..
📄️ Semiring
A semiring is like a ring but without additive inverses.
📄️ Set
Sets with elements of type K are defined as Boolean functions over K
📄️ Subgroup
A subgroup of a group G, represented as a subset that is closed under the group operations.
📄️ TwoType
A type with exactly two values.