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
|
\DOC prefixes
\TYPE {prefixes : unit -> string list}
\SYNOPSIS
Certain identifiers {c} have prefix status, meaning that combinations of the
form {c f x} will be parsed as {c (f x)} rather than the usual {(c f) x}. The
call {prefixes()} returns the list of all such identifiers.
\FAILURE
Never fails.
\EXAMPLE
In the default HOL state:
{
# prefixes();;
val it : string list = ["~"; "--"; "mod"]
}
This explains, for example, why `{~ ~ p}' parses as `{~(~p)}' rather than
parsing as `{(~ ~) p}' and generating a typechecking error.
\SEEALSO
is_prefix, parse_as_prefix, unparse_as_prefix.
\ENDDOC
|
