module Pair: sig end
cons(car(x), cdr(x)) reduces to x.
val cons : Sym.t
val car : Sym.t
val cdr : Sym.t
val is_interp : Term.t -> bool
val is_cons : Term.t -> bool
val is_car : Term.t -> bool
val is_cdr : Term.t -> bool
val mk_cons : Term.t -> Term.t -> Term.t
cons(car(x), cdr(x)) reduces to x.
val mk_car : Term.t -> Term.t
car(cons(a, _)) reduces to a.
val mk_cdr : Term.t -> Term.t
cdr(cons(_, b)) reduces to b.
Derived constructors.
val mk_tuple : Term.t list -> Term.t
val mk_proj : int -> Term.t -> Term.t
val map : (Term.t -> Term.t) -> Term.t -> Term.t
Apply term transformer f at uninterpreted positions.
val sigma : Sym.pair -> Term.t list -> Term.t
Canonization.
val mk_fresh : unit -> Term.t
Fresh variables.
val solve : Fact.equal -> Fact.equal list
Solving tuples.
val solvel : (Term.t * Term.t) list -> Fact.equal list -> Fact.equal list
val solve1 : Term.t * Term.t ->
(Term.t * Term.t) list -> Fact.equal list -> Fact.equal list
val replace_proj : Term.t -> Term.t -> Term.t -> Term.t -> Term.t
val occurs_as_arg_of_a_proj : Term.t -> Term.t -> bool
val occurs_as_arg_of_a_cons : Term.t -> Term.t -> bool
val add : Term.t * Term.t -> Fact.equal list -> Fact.equal list
val substl : Term.t -> Term.t -> Fact.equal list -> Fact.equal list
val subst1 : Term.t -> Term.t -> Term.t -> Term.t