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.