package bastet

  1. Overview
  2. Docs
Legend:
Page
Library
Module
Module type
Parameter
Class
Class type
Source

Module Bastet.InterfaceSource

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

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

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

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

Every MEDIAL_QUASIGROUP is isotopic to an ABELIAN_GROUP.

Sourcemodule type QUASIGROUP_ANY = sig ... end
Sourcemodule type LOOP = sig ... end

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

Sourcemodule type LOOP_ANY = sig ... end

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

Sourcemodule type GROUP = sig ... end

Include only either LOOP or MONOID.

Sourcemodule type GROUP_ANY = sig ... end

Include only either LOOP_ANY or MONOID_ANY.

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

Every GROUP is a LOOP.

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

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

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

Innovation. Community. Security.