package bastet

  1. Overview
  2. Docs
package bastet
Legend:
Library
Module
Module type
Parameter
Class
Class type

Note: Any data structure implementing one of these interfaces must also satisfy the corresponding laws in the corresponding Verify module.

module type TYPE = sig ... end
module type MAGMA = sig ... end
module type MEDIAL_MAGMA = sig ... end
module type MAGMA_ANY = sig ... end
module type SEMIGROUP = sig ... end
module type SEMIGROUP_ANY = sig ... end
module type MONOID = sig ... end

A MONOID only needs to be commutative with the empty element.

module type MONOID_ANY = sig ... end
module type QUASIGROUP = sig ... end
module type MEDIAL_QUASIGROUP = sig ... end

Every MEDIAL_QUASIGROUP is isotopic to an ABELIAN_GROUP.

module type QUASIGROUP_ANY = sig ... end
module type LOOP = sig ... end

A LOOP only needs to be commutative with the empty element.

module type LOOP_ANY = sig ... end

A LOOP_ANY only needs to be commutative with the empty element.

module type GROUP = sig ... end

Include only either LOOP or MONOID.

module type GROUP_ANY = sig ... end

Include only either LOOP_ANY or MONOID_ANY.

module type GROUP_LOOP = functor (G : GROUP) -> LOOP

Every GROUP is a LOOP.

module type GROUP_LOOP_ANY = functor (G : GROUP_ANY) -> LOOP_ANY

A LOOP_ANY only needs to be commutative with the empty element.

module type ABELIAN_GROUP = sig ... end
module type ABELIAN_GROUP_ANY = sig ... end
module type FUNCTOR = sig ... end
module type APPLY = sig ... end
module type APPLICATIVE = sig ... end
module type MONAD = sig ... end
module type ALT = sig ... end
module type PLUS = sig ... end
module type ALTERNATIVE = sig ... end
module type FOLDABLE = sig ... end
module type UNFOLDABLE = sig ... end
module type TRAVERSABLE = sig ... end
module type TRAVERSABLE_F = functor (A : APPLICATIVE) -> TRAVERSABLE with type 'a applicative_t = 'a A.t
module type SEMIGROUPOID = sig ... end
module type CATEGORY = sig ... end
module type EQ = sig ... end
module type QUASIREFLEXIVE_EQ = sig ... end
module type EQ1 = sig ... end
module type EQ2 = sig ... end
type ordering = [
  1. | `less_than
  2. | `equal_to
  3. | `greater_than
]
val invert : [< `equal_to | `greater_than | `less_than ] -> [> `equal_to | `greater_than | `less_than ]
val int_to_ordering : int -> [> `equal_to | `greater_than | `less_than ]
val unsafe_compare : 'a -> 'b -> [> `equal_to | `greater_than | `less_than ]
module type ORD = sig ... end
module Ordering (O : ORD) : sig ... end
module type BOUNDED = sig ... end
module type JOIN_SEMILATTICE = sig ... end
module type MEET_SEMILATTICE = sig ... end
module type BOUNDED_JOIN_SEMILATTICE = sig ... end
module type BOUNDED_MEET_SEMILATTICE = sig ... end
module type LATTICE = sig ... end
module type BOUNDED_LATTICE = sig ... end
module type DISTRIBUTIVE_LATTICE = sig ... end
module type BOUNDED_DISTRIBUTIVE_LATTICE = sig ... end
module type HEYTING_ALGEBRA = sig ... end
module type INVOLUTIVE_HEYTING_ALGEBRA = sig ... end
module type BOOLEAN_ALGEBRA = sig ... end
module type SHOW = sig ... end
module type SEMIRING = sig ... end
module type RING = sig ... end
module type COMMUTATIVE_RING = sig ... end
module type DIVISION_RING = sig ... end
module type EUCLIDEAN_RING = sig ... end
module type FIELD = sig ... end
module type INVARIANT = sig ... end
module type CONTRAVARIANT = sig ... end
module type PROFUNCTOR = sig ... end
module type MONAD_ZERO = sig ... end
module type MONAD_PLUS = sig ... end
module type EXTEND = sig ... end
module type COMONAD = sig ... end
module type BIFUNCTOR = sig ... end
module type BIAPPLY = sig ... end
module type BIAPPLICATIVE = sig ... end
module type BIFOLDABLE = sig ... end
module type BITRAVERSABLE = sig ... end
module type BITRAVERSABLE_F = functor (A : APPLICATIVE) -> BITRAVERSABLE with type 'a applicative_t = 'a A.t
module type BICONTRAVARIANT = sig ... end