module Subst: Var.Subst
type 'a var = 'a Var.t
type (+'ty, +'a) t
A substitution for variables of type 'ty, to terms 'a
val empty : ('a, 'b) t
val is_empty : ('a, 'b) t -> bool
val size : ('a, 'b) t -> int
val singleton : 'ty var -> 'a -> ('ty, 'a) t
val add : subst:('ty, 'a) t ->
'ty var -> 'a -> ('ty, 'a) t
val add_list : subst:('ty, 'a) t ->
'ty var list -> 'a list -> ('ty, 'a) t
add_list ~subst v t add each binding v_i -> t_i to the subst.
Raises Invalid_argument if List.length v <> List.length t
val concat : ('ty, 'a) t -> into:('ty, 'a) t -> ('ty, 'a) t
concat s ~into:s2 adds every binding of s into s2
val of_list : 'ty var list -> 'a list -> ('ty, 'a) t
of_list vars l = add_list ~subst:empty vars l
val remove : subst:('ty, 'a) t -> 'ty var -> ('ty, 'a) t
Remove binding for this variable.
careful if other bindings depend on this variable's binding...
val deref_rec : subst:('ty, 'ty var) t ->
'ty var -> 'ty var
For renamings, follow the substitution until we find an unbound var
val find_deref_rec : subst:('ty, 'ty var) t ->
'ty var -> 'ty var option
find_deref_rec ~subst v returns Some (deref_rec subst v') if v
is bound, or None otherwise
val rename_var : ('a, 'a var) t ->
'a var -> ('a, 'a var) t * 'a var
rename_var subst v returns subst', v' where v' is
a fresh copy of v, and subst' = add v v' subst
val mem : subst:('ty, 'a) t -> 'ty var -> bool
val find : subst:('ty, 'a) t -> 'ty var -> 'a option
val find_exn : subst:('ty, 'a) t -> 'ty var -> 'a
Raises Not_found if var not bound
val find_or : subst:('ty, 'a) t -> default:'a -> 'ty var -> 'a
val map : f:('a -> 'b) -> ('ty, 'a) t -> ('ty, 'b) t
val to_list : ('ty, 'a) t -> ('ty var * 'a) list
val to_seq : ('ty, 'a) t -> ('ty var * 'a) Sequence.t
val print : 'a CCFormat.printer -> ('b, 'a) t CCFormat.printer