Module `Logtk.PatternUnif`

Pattern unification algorithm implementation

module US = Unif_subst

type subst = US.t

module S : sig ... end

exception NotUnifiable
exception NotInFragment

val eta_expand_otf : subst:subst -> scope:Scoped.scope -> Type.t list -> Type.t list -> Term.t -> Term.t -> Term.t * Term.t * Type.t list
val norm_deref : Unif_subst.t -> Term.t Scoped.t -> Term.t
val unif_simple : ?⁠subst:Subst.t -> scope:int -> Term.t -> Term.t -> US.t option
val unify_scoped : ?⁠subst:subst -> ?⁠counter:int Stdlib.ref -> Term.t Scoped.t -> Term.t Scoped.t -> subst