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