Module Term


module Term: sig .. end

Term data structure




type term =
| Var of Var.var
| App of Symb.symbol * term list
val vars : term -> Var.VarSet.t
val vars_of_terms : term list -> Var.VarSet.t
val list_vars : term -> Var.var list
val list_vars_of_terms : term list -> Var.var list
val is_linear : term -> bool
val symbols : term -> Symb.SymbolSet.t
val symbols_of_terms : term list -> Symb.SymbolSet.t
val occurs : Var.var -> term -> bool
val fprintf : Format.formatter -> term -> unit
val rename : Var.var Var.VarMap.t -> term -> term
val compare : term -> term -> int
Comparison of terms modulo variable renaming
val eq : term -> term -> bool
val linearize : term -> term * Var.var Var.VarMap.t
Linearize a term
val pr_term : Format.formatter -> term -> unit
Pretty print.