REFL_TAC : tactic
SYNOPSIS
Solves a goal that is an equation between alpha-equivalent terms.
DESCRIPTION
When applied to a goal
A ?- t = t'
, where
t
and
t'
are alpha-equivalent,
REFL_TAC
completely solves it.
A ?- t = t' ============= REFL_TAC
FAILURE CONDITIONS
Fails unless the goal is an equation between alpha-equivalent terms.
SEE ALSO
ACCEPT_TAC
,
MATCH_ACCEPT_TAC
,
REWRITE_TAC
.