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.