Module Sl

module Sl: sig  end

Fold over the find structure.

type t = (Term.t * Fact.justification option) Term.Map.t

val empty : 'a Term.Map.t

val is_empty : 'a Term.Map.t -> bool

Parameters:

s : 'a Term.Map.t

val eq : 'a -> 'a -> bool

Parameters:

s	:	`'a`
t	:	`'a`

val fold : (Term.Map.key -> 'a -> 'b -> 'b) -> 'a Term.Map.t -> 'b -> 'b

Fold over the find structure.

val to_list : ('a * 'b) Term.Map.t -> (Term.Map.key * 'a) list

Solution set

Parameters:

s : ('a * 'b) Term.Map.t

Pretty-printer.

val pp : Format.formatter -> (Term.Map.key * 'a) Term.Map.t -> unit

Parameters:

fmt	:	`Format.formatter`
s	:	`(Term.Map.key * 'a) Term.Map.t`

val apply : ('a * 'b) Term.Map.t -> Term.Map.key -> 'a

Parameters:

s	:	`('a * 'b) Term.Map.t`
x	:	`Term.Map.key`

val find : (Term.Map.key * 'a) Term.Map.t -> Term.Map.key -> Term.Map.key

Parameters:

s	:	`(Term.Map.key * 'a) Term.Map.t`
x	:	`Term.Map.key`

val mem : 'a Term.Map.t -> Term.Map.key -> bool

Parameters:

s	:	`'a Term.Map.t`
x	:	`Term.Map.key`

val update : Fact.equal ->
       (Term.t * Fact.justification option) Term.Map.t ->
       (Term.t * Fact.justification option) Term.Map.t

Parameters:

e	:	`Fact.equal`
s	:	`(Term.t * Fact.justification option) Term.Map.t`

val restrict : Term.Map.key -> 'a Term.Map.t -> 'a Term.Map.t