install_parser : string * (lexcode list -> preterm * lexcode list) -> unit
- SYNOPSIS
-
Install a user parser.
- DESCRIPTION
-
HOL Light allows user parsing functions to be installed, and will try them on
all terms during parsing before the usual parsers. The call
install_parser(s,p) installs the parser p among the user parsers to try in
this way. The string s is there so that the parser can conveniently be
deleted again.
- FAILURE CONDITIONS
-
Never fails.
- SEE ALSO
-
delete_parser, installed_parsers, try_user_parser.