subst_assoc : ('a -> bool) -> ('a,'b)subst -> 'b option
STRUCTURE
SYNOPSIS
Treats a substitution as an association list.
DESCRIPTION
An application subst_assoc P [{redex_1,residue_1},...,{redex_n,residue_n}] returns SOME residue_i if P holds of redex_i, and did not hold (or fail) for {redex_j | 1 <= j < i}. If P holds for none of the redexes in the substitution, NONE is returned.
FAILURE
If P redex_i fails for some redex encountered in the left-to-right traversal of the substitution.
EXAMPLE
- subst_assoc is_abs [T |-> F, Term `\x.x` |-> Term `combin$I`];
> val it = SOME`I` : term option

SEEALSO
HOL  Kananaskis-14