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
26
27
28
29
30
31
32
33
34
|
\DOC try_user_printer
\TYPE {try_user_printer : formatter -> term -> unit}
\SYNOPSIS
Try user-defined printers on a term.
\DESCRIBE
HOL Light allows arbitrary user printers to be inserted into the toplevel
printer so that they are invoked on all applicable subterms (see
{install_user_printer}). The call {try_user_printer fmt tm} attempts all
installed user printers on the term {tm} in an implementation-defined order,
sending output to the formatter {fmt}. If one succeeds, the call returns {()},
and otherwise it fails.
\FAILURE
Fails if no user printer is applicable to the given term (e.g. if no user
printers have been installed).
\EXAMPLE
After installing the printer for variables with types in the example for
{install_user_printer}, you can try:
{
# try_user_printer std_formatter `x:num`;;
(x:num)val it : unit = ()
# try_user_printer std_formatter `1`;;
Exception: Failure "tryfind".
}
\SEEALSO
delete_user_printer, install_user_printer.
\ENDDOC
|
