Combinators_base (p.libzipperposition.2.0.doc.libzipperposition.Libzipperposition.Combinators

exception IsNotCombinator

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