Module `Libzipperposition.Combinators_base`

val mk_s : ?⁠args:Logtk.Term.t list -> alpha:Logtk.Term.t -> beta:Logtk.Term.t -> gamma:Logtk.Term.t -> Logtk.Term.t
val mk_b : ?⁠args:Logtk.Term.t list -> alpha:Logtk.Term.t -> beta:Logtk.Term.t -> gamma:Logtk.Term.t -> Logtk.Term.t
val mk_c : ?⁠args:Logtk.Term.t list -> alpha:Logtk.Term.t -> beta:Logtk.Term.t -> gamma:Logtk.Term.t -> Logtk.Term.t
val mk_k : ?⁠args:Logtk.Term.t list -> alpha:Logtk.Term.t -> beta:Logtk.Term.t -> Logtk.Term.t
val mk_i : ?⁠args:Logtk.Term.t list -> alpha:Logtk.Term.t -> Logtk.Term.t
val bunder_optimizations : (Logtk.Term.t -> Logtk.Term.t option) list
val curry_optimizations : (Logtk.Term.t -> Logtk.Term.t option) list
val narrow_rules : (Logtk.Term.t -> Logtk.Term.t option) list
val abf : rules:(Logtk.Term.t -> Logtk.Term.t option) list -> Logtk.Lambda.term -> Logtk.Term.t
val comb2lam : Logtk.Term.t -> Logtk.Term.t
val comb_normalize : Logtk.Term.t -> Logtk.Term.t CCOpt.t
val cmp_by_max_weak_r_len : Logtk.Term.t -> Logtk.Term.t -> Logtk.Comparison.t * Logtk.Term.t * Logtk.Term.t
val narrow : Logtk.Term.t -> Logtk.Term.t