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
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
|
\DOC help
\TYPE {help : string -> unit}
\SYNOPSIS
Displays help on a given identifier in the system.
\DESCRIBE
A call {help "s"} will attempt to display the help file associated with a
particular identifier {s} in the system. If there is no entry for identifier
{s}, the call responds instead with some possibly helpful suggestions as to
what you might have meant, based on a simple `edit distance' criterion.
The built-in help files are stored in the {Help} subdirectory of HOL Light.
Users can add additional locations by modifying {help_path}. Normally the help
file for an identifier {name} would be called {name.doc}, but there are a few
exceptions, because some identifiers have characters that cannot be put in
filenames and some platforms like Cygwin have inadequate case sensitivity.
\FAILURE
Never fails.
\EXAMPLE
Here is a successful call:
{
# help "lhs";;
-------------------------------------------------------------------
lhs : term -> term
SYNOPSIS
Returns the left-hand side of an equation.
DESCRIPTION
lhs `t1 = t2` returns `t1`.
FAILURE CONDITIONS
Fails with lhs if the term is not an equation.
EXAMPLES
# lhs `2 + 2 = 4`;;
val it : term = `2 + 2`
SEE ALSO
dest_eq, lhand, rand, rhs.
-------------------------------------------------------------------
val it : unit = ()
}
\noindent and here is one for a non-existent identifier:
{
# help "IMP_TAC";;
-------------------------------------------------------------------
No help found for "IMP_TAC"; did you mean:
help "SIMP_TAC";;
help "MP_TAC";;
help "IMP_TRANS";;
?
--------------------------------------------------------------------
}
\SEEALSO
help_path, hol_version.
\ENDDOC
|
