Previous  Up  Next

Module Coproduct


module Coproduct: sig  end
Fold iterator
val inl : Sym.t
val inr : Sym.t
val outl : Sym.t
val outr : Sym.t
val is_interp : Term.t -> bool
Parameters:
?? : Term.t

Fold iterator

val fold : (Term.t -> 'a -> 'b) -> Term.t -> 'a -> 'b
Parameters:
f : Term.t -> 'a -> 'b
a : Term.t
e : 'a

Constructors for tuples and projections.

val mk_inl : Term.t -> Term.t
val mk_inr : Term.t -> Term.t
val mk_outr : Term.t -> Term.t
val mk_outl : Term.t -> Term.t
val mk_inj : int -> Term.t -> Term.t
Parameters:
i : int
x : Term.t
 
val mk_out : int -> Term.t -> Term.t
Parameters:
i : int
x : Term.t

Two chains of injections are disequal if they differ.

val is_diseq : Term.t -> Term.t -> bool
Parameters:
a : Term.t
b : Term.t

Sigmatizing.

val sigma : Sym.coproduct -> Term.t list -> Term.t
Parameters:
op : Sym.coproduct
l : Term.t list

Apply term transformer f at uninterpreted positions.

val map : (Term.t -> Term.t) -> Term.t -> Term.t
Parameters:
f : Term.t -> Term.t
a : Term.t

Solving tuples.

val solve : Fact.equal -> Fact.equal list
Parameters:
e : Fact.equal
 
val solvel : (Term.t * Term.t) list -> Fact.equal list -> Fact.equal list
Parameters:
el : (Term.t * Term.t) list
sl : Fact.equal list
 
val solve1 : Term.t * Term.t ->
       (Term.t * Term.t) list -> Fact.equal list -> Fact.equal list
Parameters:
(a,b) : Term.t * Term.t
el : (Term.t * Term.t) list
sl : Fact.equal list
 
val solvevar : Term.t * Term.t ->
       (Term.t * Term.t) list -> Fact.equal list -> Fact.equal list
Parameters:
(x,b) : Term.t * Term.t
el : (Term.t * Term.t) list
sl : Fact.equal list
 
val add : Term.t * Term.t -> Fact.equal list -> Fact.equal list
Parameters:
(a,b) : Term.t * Term.t
sl : Fact.equal list
 
val substl : Term.t -> Term.t -> Fact.equal list -> Fact.equal list
Parameters:
a : Term.t
b : Term.t
 
val subst1 : Term.t -> Term.t -> Term.t -> Term.t
Parameters:
a : Term.t
x : Term.t
b : Term.t