match_type

Type.match_type : hol_type -> hol_type -> (hol_type,hol_type) subst

Calculates a substitution theta such that instantiating the first argument with theta equals the second argument.

If match_type ty1 ty2 succeeds, then

    type_subst (match_type ty1 ty2) ty1 = ty2

Failure

If no such substitution can be found.

Example

> match_type alpha (Type`:num`);
val it = [{redex = “:α”, residue = “:num”}]: (hol_type, hol_type) Lib.subst

> let val patt = Type`:('a -> bool) -> 'b`
     val ty =   Type`:(num -> bool) -> bool`
  in
    type_subst (match_type patt ty) patt = ty
  end;
val it = true: bool

> match_type (alpha --> alpha)
           (ind   --> bool);
Exception- HOL_ERR (at Type.raw_match_type: double bind on type variable 'a) raised

See also

Term.match_term, Type.type_subst