module Sigma: sig
.. end
type
t = {
|
dvar : Lang.F.Vars.t ; |
|
dcod : Lang.F.Vars.t ; |
|
dall : Lang.F.Vars.t ; |
|
def : Lang.F.term Lang.F.Vmap.t ; |
|
ceq : Ceq.t ; |
|
cst : Lang.F.term Lang.F.Tmap.t ; |
|
mutable mem : Lang.F.term Lang.F.Tmap.t array ; |
}
val empty : t
val equal : t -> t -> bool
val mem : Lang.F.Vmap.key -> t -> bool
val find : Lang.F.Vmap.key -> t -> Lang.F.term
val iter : (Lang.F.Vmap.key -> Lang.F.term -> unit) -> t -> unit
val e_apply : t -> Lang.F.term -> Lang.F.term
val p_apply : t -> Lang.F.pred -> Lang.F.pred
val add : Lang.F.Vmap.key -> Lang.F.term -> t -> t
val domain : t -> Lang.F.Vars.t
val codomain : t -> Lang.F.Vars.t
val class_of : t -> Ceq.elt -> Ceq.elt list
val assume : t -> Lang.F.pred -> t
val pretty : string -> Format.formatter -> t -> unit