ABS_TAC

Tactic.ABS_TAC : tactic

Strips lambda abstraction on both sides of an equation.

When applied to a goal of the form A ?- (\x. M) = (\y. N) (where M and N may or may not mention their respective bound variables), the tactic ABS_TAC strips away the lambda abstractions:

    A ?- (\x. f x) = (\y. g y)
   ============================  ABS_TAC
            A ?- f x = g x

Failure

Fails unless the goal has the above form, namely an equation both sides of which consist of a lamdba abstraction.

Comments

When the lambda abstractions’ bound variables conflict with existing free variables in the goal, variants of those names may occur in the goal that results.

See also

Tactic.AP_TERM_TAC, Tactic.AP_THM_TAC