ShiftWithJoin (mugen.Mugen.ShiftWithJoin)

module type Semilattice = sig ... end

The signature of a displacement algebra with binary joins. (Note that this refers to joins of displacements, not joins of universe levels.)

module type BoundedSemilattice = sig ... end

A displacement algebra with joins and a bottom element.

module Nat : sig ... end

Natural numbers with addition. Caveats: it does not handle integer overflow.

module Int : sig ... end

Integers with addition. Caveats: it does not handle integer overflow.

module NonPositive : sig ... end

Non-positive integers with addition. Caveats: it does not handle integer overflow.

module Product (X : Semilattice) (Y : Semilattice) : sig ... end

Binary products.

module Lexicographic
  (X : BoundedSemilattice)
  (Y : BoundedSemilattice) : 
  sig ... end

Binary products, but with the lexicographical order.

module NearlyConstant (Base : BoundedSemilattice) : sig ... end

Infinite products with finite elements different from a fixed displacement.

module FiniteSupport (Base : Semilattice) : sig ... end

Infinite products with finite supports. A special case of NearlyConstant.