print_type_as_tex : hol_type -> unit
STRUCTURE
SYNOPSIS
Prints a type as LaTeX.
DESCRIPTION
An invocation of print_type_as_tex ty will print the type ty, replacing various character patterns (e.g. # and ->) with LaTeX commands. The translation is controlled by the string to string function EmitTeX.hol_to_tex.
FAILURE
Should never fail.
EXAMPLE
 - EmitTeX.print_type_as_tex ``:bool # bool -> num`` before print "\n";
 :bool \HOLTokenProd{} bool \HOLTokenMap{} num
 > val it = () : unit
COMMENTS
The LaTeX style file holtexbasic.sty (or holtex.sty) should be used and the output should be pasted into a Verbatim environment.
SEEALSO
HOL  Kananaskis-14