Module `Logtk.PUnif`

Pragmatic variant of JP algorithm

module IntSet : CCSet.S with type IntSet.elt = CCInt.t

val elim_subsets_rule : ?⁠max_elims:int option -> elim_vars:IntSet.t Stdlib.ref -> counter:IntSet.elt Stdlib.ref -> scope:Scoped.scope -> Term.t -> Term.t -> int -> (Subst.FO.t * int) OSeq.t
val proj_hs : counter:int Stdlib.ref -> scope:Scoped.scope -> flex:Term.t -> Term.t -> Subst.FO.t CCList.t

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