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
41
|
\DOC FAIL_TAC
\TYPE {FAIL_TAC : string -> tactic}
\SYNOPSIS
Tactic that always fails, with the supplied string.
\KEYWORDS
tactic.
\DESCRIBE
Whatever goal it is applied to, {FAIL_TAC "s"} always fails with {Failure "s"}.
\FAILURE
The application of {FAIL_TAC} to a string never fails; the resulting
tactic always fails.
\EXAMPLE
The following example uses the fact that if a tactic {t1} solves
a goal, then the tactic {t1 THEN t2} never results in the application
of {t2} to anything, because {t1} produces no subgoals. In attempting
to solve the following goal:
{
# g `if x then T else T`;;
}
\noindent the tactic
{
# e(REWRITE_TAC[] THEN FAIL_TAC "Simple rewriting failed to solve goal");;
Exception: Failure "Simple rewriting failed to solve goal".
}
\noindent fails with the message provided, whereas the following quietly solves
the goal:
{
# e(REWRITE_TAC[COND_ID] THEN FAIL_TAC "Using that failed to solve goal");;
val it : goalstack = No subgoals
}
\SEEALSO
ALL_TAC, NO_TAC.
\ENDDOC
|
