disch

HolKernel.disch : ((term * term list) -> term list)

Removes those elements of a list of terms that are alpha equivalent to a given term.

Given a pair (t,tl) of term t and term list tl, disch removes those elements of tl that are alpha equivalent to t.

Example

> disch (``\x:bool.T``, [``A = T``, ``B = 3``, ``\y:bool.T``]);
val it = [``A = T``,``B = 3``] : term list

See also

Lib.filter