Eliminates a let binding in a goal by introducing equational assumptions.
DESCRIPTION
Given a goal A ?- t where t contains a free let-expression
let x1 = E1 and ... let xn = En in E, the tactic LET_TAC replaces that
subterm by simply E but adds new assumptions E1 = x1, ..., En = xn.
That is, the local let bindings are replaced with new assumptions, put in
reverse order so that ASM_REWRITE_TAC will not immediately expand them. In
cases where the term contains several let-expression candidates, a topmost one
will be selected. In particular, if let-expressions are nested, the outermost
one will be handled.
FAILURE CONDITIONS
Fails if the goal contains no eligible let-term.
EXAMPLE
# g `let x = 2 and y = 3 in x + 1 <= y`;;
val it : goalstack = 1 subgoal (1 total)
`let x = 2 and y = 3 in x + 1 <= y`
# e LET_TAC;;
val it : goalstack = 1 subgoal (1 total)
0 [`2 = x`]
1 [`3 = y`]
`x + 1 <= y`