1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
|
\DOC LET_TAC
\TYPE {LET_TAC : tactic}
\SYNOPSIS
Eliminates a let binding in a goal by introducing equational assumptions.
\DESCRIBE
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
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`
}
\SEEALSO
ABBREV_TAC, EXPAND_TAC, let_CONV.
\ENDDOC
|
