package alt-ergo-lib

You can search for identifiers within the package.

in-package search v0.2.0

The Alt-Ergo SMT prover library

Install

sha256=39e2c9128a7d1e89f332e31a2716f359f3b9e1a925fe81f11fa4a749b5d24d82

sha512=ca953fe5a4964287de7e328ec4e3724a9baaa908c22862b075da5870bbf3707c7f78bd9fe0af98ee6c6382b5de0a4ddfcc93e09dc8b5b8e7d6ab6b1196a0656d

This module provides a registry type to access and update a single "current" instance associated with multiple global domain types.

type t

Maps global domain modules (of type 'a global_domain) to an associated domain of the corresponding type 'a.

val empty : t

empty maps all domain modules D to their default domain D.empty.

val find : 'a global_domain -> t -> 'a

find (module D) t returns the global domain associated with the domain module D. Defaults to D.empty.

val add : 'a global_domain -> 'a -> t -> t

add (module D) d t registers the global domain d for the domain module D. Overwrite any pre-existing global domain associated with D.