Module `Libzipperposition_calculi.Rewriting`

module Make : functor (E : Libzipperposition.Env_intf.S) -> sig ... end

val unfold_def_before_cnf : ((Logtk.TypedSTerm.t, Logtk.TypedSTerm.t, Logtk.TypedSTerm.t) Logtk.Statement.t, 'c) CCVector.t -> ((Logtk.TypedSTerm.t, Logtk.TypedSTerm.t, Logtk.TypedSTerm.t) Logtk.Statement.t, 'c) CCVector.t
val extension : Libzipperposition.Extensions.t