sig
type ty = InnerTerm.t
type term = InnerTerm.t
val bind :
Unif_intf.subst -> ty HVar.t Scoped.t -> term Scoped.t -> Unif_intf.subst
val unification :
?subst:Unif_intf.subst ->
term Scoped.t -> term Scoped.t -> Unif_intf.subst
val matching :
?subst:Unif_intf.subst ->
pattern:term Scoped.t -> term Scoped.t -> Unif_intf.subst
val matching_same_scope :
?protect:ty HVar.t Sequence.t ->
?subst:Unif_intf.subst ->
scope:int -> pattern:term -> term -> Unif_intf.subst
val matching_adapt_scope :
?protect:ty HVar.t Sequence.t ->
?subst:Unif_intf.subst ->
pattern:term Scoped.t -> term Scoped.t -> Unif_intf.subst
val variant :
?subst:Unif_intf.subst ->
term Scoped.t -> term Scoped.t -> Unif_intf.subst
val equal : subst:Unif_intf.subst -> term Scoped.t -> term Scoped.t -> bool
val are_unifiable : term -> term -> bool
val matches : pattern:term -> term -> bool
val are_variant : term -> term -> bool
end