Module Unifier.MakeSource

Parameters

module H : HOLES

Signature

Sourcetype t
Sourceval make : H.t -> t
Sourceval context : t -> H.t
Sourceval push : Term.typ -> t -> t
Sourceval unify0 : Term.typ -> Term.typ -> bool -> t -> t option
Sourceval unify : Term.typ -> Term.typ -> bool -> H.t -> H.t option

unify act req is_super gh

Unify the type act with the type req using gh as the context with holes.

is_super indicates if the typ req can be regarded as a supertype of act.