type_match : hol_type -> hol_type -> (hol_type * hol_type) list -> (hol_type * hol_type) list

SYNOPSIS

Computes a type instantiation to match one type to another.

DESCRIPTION

The call type_match vty cty [] will if possible find an instantiation of the type variables in vty to make it the same as cty, and will fail if this is not possible. The instantiation is returned in a list of term-variable pairs as expected by type instantiation operations like inst and INST_TYPE. More generally, type_match vty cty env will attempt to find such a match assuming that the instantiations already in the list env are needed (this is helpful, for example, in matching multiple pairs of types in parallel).

FAILURE CONDITIONS

Fails if there is no match under the chosen constraints.

EXAMPLE

Here is a basic example with an empty last argument:

  # type_match `:A->B->bool` `:num->num->bool` [];;
  val it : (hol_type * hol_type) list = [(`:num`, `:A`); (`:num`, `:B`)]

and here is an illustration of how the extra argument can be used to perform parallel matches.

  # itlist2 type_match
      [`:A->A->bool`; `:B->B->bool`] [`:num->num->bool`; `:bool->bool->bool`]
      [];;
  val it : (hol_type * hol_type) list = [(`:num`, `:A`); (`:bool`, `:B`)]

SEE ALSO

inst, INST_TYPE, mk_mconst, term_match.