free_in : term -> term -> bool
Tests if one term is free in another.
When applied to two terms t1 and t2, the function free_in returns
true if t1 is free in t2, and false otherwise. It is not necessary
that t1 be simply a variable.
- FAILURE CONDITIONS
In the following example free_in returns false because the x in SUC x
in the second term is bound:
whereas the following call returns true because the first instance
of x in the second term is free, even though there is also a bound instance:
# free_in `SUC x` `!x. SUC x = x + 1`;;
val it : bool = false
# free_in `x:bool` `x /\ (?x. x=T)`;;
val it : bool = true
If the term t1 is a variable, the rule vfree_in is more basic and probably
- SEE ALSO
frees, freesin, freesl, thm_frees, vfree_in.