is_reserved_word : string -> bool
SYNOPSIS
Tests if a string is one of the reserved words.
DESCRIPTION
Certain identifiers in HOL are reserved, e.g. `
if
', `
let
' and `
|
', meaning that they are special to the parser and cannot be used as ordinary identifiers. The call
is_reserved_word s
tests if the string
s
is one of them.
FAILURE CONDITIONS
Never fails.
SEE ALSO
reserved_words
,
reserve_words
,
unreserve_words
.