1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
|
\DOC try_user_parser
\TYPE {try_user_parser : lexcode list -> preterm * lexcode list}
\SYNOPSIS
Try all user parsing functions.
\DESCRIBE
HOL Light allows user parsing functions to be installed, and will try them on
all terms during parsing before the usual parsers. The call
{try_user_parser l} attempts to parse the list of tokens {l} using all the user
parsers, taking the results from whichever one succeeds first.
\FAILURE
Fails if all user parsers fail.
\SEEALSO
delete_parser, install_parser, installed_parsers.
\ENDDOC
|
