module App: sig end
Operations on term applications.
val mk_const : Sym.t -> Term.t
mk_const c constructs a function application of symbol c to the empty
argument list.
val mk_app : Sym.t -> Term.t list -> Term.t
mk_app f l constructs a function application of symbol f to a list l.
val destruct : Term.t -> Sym.t * Term.t list
destruct a destructure an application a of the form
App(f, l) into (f, l).
val sym_of : Term.t -> Sym.t
sym_of a returns the function symbol f of an application
a of the form App(f,_).
val theory_of : Term.t -> Th.t
theory_of a returns the theory associated with the top-level
function symbol of a, and raises Not_found otherwise.
val args_of : Term.t -> Term.t list
sym_of a returns the argument list l of an application
a of the form App(_,l, _).