Module Lattices.CongruenceSource

The congruence lattice: abstracts integers by modular constraints of the form x ≡ a (mod n). Captures properties like even/odd or divisibility.

Sourcetype t = Z.t * Z.t
Sourceval compare : (Z.t * Z.t) -> (Z.t * Z.t) -> int
Sourceval equal : (Z.t * Z.t) -> (Z.t * Z.t) -> bool
Sourceval hash : (Z.t * Z.t) -> int
Sourceval bottom : size:'a -> unit -> Z.t * Z.t
Sourceval top : size:'a -> unit -> Z.t * Z.t
Sourceval singleton : size:int -> Z.t -> Z.t * Z.t