type unif_subst = Unif_subst.ttype subst = Subst.ttype term = InnerTerm.ttype ty = InnerTerm.tval _allow_pattern_unif : bool refval _unif_bool : bool refval occurs_check :
depth:int ->
subst ->
InnerTerm.t HVar.t Scoped.t ->
InnerTerm.t Scoped.t ->
boolval unif_array_com :
?size:[ `Same | `Smaller ] ->
'subst ->
op:('subst -> 'a Scoped.t -> 'a Scoped.t -> 'subst Iter.t) ->
'a array Scoped.t ->
'a array Scoped.t ->
'subst Iter.tGeneric unification over two arrays (of the same size, or the first one must be smaller or equal)
val unif_list :
'subst ->
op:('subst -> 'a Scoped.t -> 'a Scoped.t -> 'subst Iter.t) ->
'a list Scoped.t ->
'a list Scoped.t ->
'subst Iter.tGeneric unification over two lists (of the same size)
val unif_list_com :
?size:[ `Same | `Smaller ] ->
'subst ->
op:('subst -> 'a Scoped.t -> 'a Scoped.t -> 'subst Iter.t) ->
'a list Scoped.t ->
'a list Scoped.t ->
'subst Iter.tGeneric unification over two lists (of the same size or smaller)
in HO, we have f1 l1 and f2 l2, where application is left-associative. we need to unify from the right (the outermost application is on the right) so this returns pairs to unify (including heads).
in HO, we have l1 -> ret1 and l2 -> ret2, where -> is right-associative. we need to unify from the left, so this returns pairs to unify (including return types).
module type S = Unif_intf.Smodule Inner : S with type term = InnerTerm.t and type ty = InnerTerm.tTo be used only on terms without InnerTerm.Multiset constructor
module Ty : sig ... endmodule FO : sig ... end