module Coproduct: sig end
Operation on function symbols of the
coproduct theory
Th.cop.
mk_inl, mk_inf, mk_outl and mk_outr are the function symbols
representing In(Left), In(Right), Out(Right), and Out(Left), respectively.get f returns the function symbol in Th.cop represented by f,
or raises Not_found. - The tests
is_inl f, is_inr f, is_outl f, and is_outr succeed iff f
represents InL, In(Right), Out(Left), or Out(Right), respectively.
pp p fmt (op, [a]) pretty-prints the appliation of op to the
unary list [a] depending on the value of Pretty.flag. See
also Pretty.apply.
val mk_inl : Sym.t
val mk_inr : Sym.t
val mk_outl : Sym.t
val mk_outr : Sym.t
val get : Sym.t -> Sym.coproduct
val is : Sym.t -> bool
val is_inl : Sym.t -> bool
val is_inr : Sym.t -> bool
val is_outl : Sym.t -> bool
val is_outr : Sym.t -> bool
val pp : 'a Pretty.printer -> (Sym.coproduct * 'a list) Pretty.printer