try_user_printer : formatter -> term -> unit

SYNOPSIS

Try user-defined printers on a term.

DESCRIPTION

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 CONDITIONS

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".