Module Letify.Sigma

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