module type I = sig .. end
type
type
val anonymous : var
An "unidentified" variable
val is_anonymous : var Fun.predicate
is_unnamed v returns true if and only if v is anonymous
val mk : string -> var
mk_var n exist returns a variable with name n; if exist is true then
the returned variable will be existential, otherwise it will be free. If the
VarManager already knows about a variable named n, then this will be returned,
otherwise it will generate a fresh variable.
val is_exist_var : var Fun.predicate
is_exist_var v returns true if and only if v is an existential variable.
val is_free_var : var Fun.predicate
is_exist_var v returns true if and only if v is a free variable.
val fresh_evar : var_container -> var
fresh_evar s returns an existential variable that is fresh for the set of variables s.
val fresh_evars : var_container -> int -> var list
fresh_evars s n returns n distinct existential variables that are all fresh for the set of variables s.
val fresh_fvar : var_container -> var
fresh_uvar s returns a free variable that is fresh for the set of variables s.
val fresh_fvars : var_container -> int -> var list
fresh_uvars s n returns n distinct free variables that are all fresh for the set of variables s.