Module Theo.LeqSource

The theory of linear order (<=, <, =, <>).

Parameters

module C : Comparable

Signature

Sourcetype kind
Sourcetype _ t =
  1. | Bound : {
    1. limit : C.t;
    2. inclusive : bool;
    } -> kind t
include Primitive_theory with type kind := kind and type 'kind t := 'kind t and type elt = C.t
include Theory with type 'kind t := 'kind t
Sourceval equal : _ t -> _ t -> bool

Equality check for atoms. Must be consistent with compare and hash.

Sourceval compare : _ t -> _ t -> int

Total ordering function. Used for set/map operations and canonical ordering in BDDs.

Sourceval hash : _ t -> int

Hash function for atoms. Must be compatible with equal.

Sourceval to_string : _ t -> string

String representation for debugging.

Sourcetype elt = C.t
Sourcemodule Syntax (F : Formula with type 'kind desc = 'kind t) : sig ... end