Module type Solution.EXT

module type EXT = sig  end

An equality theory is specified by means of

its name th,
a term map f a for replacing uninterpreted positions x of a with f x and canonizing the resulting term in theory th.
side effects when updating and restricting solution sets.

type t

val pp : t Pretty.printer

val empty : t

val update : t -> Fact.Equal.t -> t

Parameters:

?	:	`t`
?	:	`Fact.Equal.t`

val restrict : t -> Fact.Equal.t -> t

Parameters:

?	:	`t`
?	:	`Fact.Equal.t`