module Cl: sig end
Operation on function symbols of the theory
Th.app of
combinatory logic with case split.
- Constructors
mk_apply r and mk_abs representing
Apply(r) and Abs, respectively.
get f returns the function symbol in Th.app represented by f,
or raises Not_found. - The test
is_apply f (is_abs f) succeeds iff f
represents some Apply(r) (Abs).
pp p fmt (op, al) pretty-prints the appliation of op to the
argument list al depending on the value of Pretty.flag. See
also Pretty.apply. It assumes applications to Apply(.) to be
binary and Abs is unary.
val get : Sym.t -> Sym.cl
val apply : Sym.t
val s : Sym.t
val k : Sym.t
val i : Sym.t
val c : Sym.t
val reify : Sym.tsym * int -> Sym.t
val is : Sym.t -> bool
val is_apply : Sym.t -> bool
val is_s : Sym.t -> bool
val is_k : Sym.t -> bool
val is_i : Sym.t -> bool
val is_c : Sym.t -> bool
val is_reify : Sym.t -> bool
val d_reify : Sym.t -> Sym.tsym * int
val pp : 'a Pretty.printer -> (Sym.cl * 'a list) Pretty.printer