Module NegativeUnits


module NegativeUnits: sig .. end
Store for negative unit literals.


Used to represent negative unit facts, which is required for


type store 
val make_store : unit -> store
val null_store : store
val insert : store -> Fact.fact -> unit
val lookup : store -> Fact.fact -> Fact.fact
If the input fact is unifiable with a fact that has been previously inserted, that entry is returned. Otherwise Not_found is raised.
val iter_all : (Fact.fact -> unit) -> store -> unit
iter_all f store applies f to all terms in the store.
val clear : store -> unit
type state 
val obtain_state : store -> state
val install_state : state -> unit
val add_layer : state -> state