match_terml : hol_type list -> term set -> term -> term -> (term,term) subst * (hol_type,hol_type) subst

- STRUCTURE
- SYNOPSIS
- Match two terms while restricting some instantiations.
- DESCRIPTION
- An invocation match_terml avoid_tys avoid_tms pat ob (tmS,tyS), if it does not raise an exception, returns a pair of substitutions (S,T) such thatThe arguments avoid_tys and avoid_tms specify type and term variables in pat that are not allowed to become redexes in S and T.
aconv (subst S (inst T pat)) ob.

- FAILURE
- match_terml will fail if no S and T meeting the above requirements can be found. If a match (S,T) between pat and ob can be found, but elements of avoid_tys would appear as redexes in T or elements of avoid_tms would appear as redexes in S, then match_terml will also fail.
- EXAMPLE
- val (S,T) = match_terml [] empty_varset (Term `\x:'a. x = f (y:'b)`) (Term `\a. a = ~p`); > val S = [{redex = `(f :'b -> 'a)`, residue = `$~`}, {redex = `(y :'b)`, residue = `(p :bool)`}] : ... val T = [{redex = `:'b`, residue = `:bool`}, {redex = `:'a`, residue = `:bool`}] : ... - match_terml [alpha] empty_varset (* forbid instantiation of 'a *) (Term `\x:'a. x = f (y:'b)`) (Term `\a. a = ~p`); ! Uncaught exception: ! HOL_ERR - match_terml [] (HOLset.add(empty_varset,mk_var("y",beta))) (Term `\x:'a. x = f (y:'b)`) (Term `\a. a = ~p`); ! Uncaught exception: ! HOL_ERR

- SEEALSO

HOL Kananaskis-14