package bastet

  1. Overview
  2. Docs
package bastet
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.

GitHub Discord Twitter Peertube RSS
About
Changelog Releases Industrial Users Academic Users Why OCaml
Ecosystem
Packages Community Events OCaml Planet Jobs
Resources
Install OCaml Get Started Platform Tools Language Manual Standard Library API Books Exercises Papers OCaml Playground Logo
Policies
Carbon Footprint Governance Privacy Code of Conduct