package libzipperposition

  1. Overview
  2. Docs
package libzipperposition
Legend:
Library
Module
Module type
Parameter
Class
Class type
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 narrow : Logtk.Term.t -> Logtk.Term.t