Hello,
This is caused by the update to the printers back in March:
https://code.google.com/p/hol-light/source/detail?spec=svn208&r=184
Try this instead:
let print_typed_var fmt tm =
let s,ty = dest_var tm in
pp_print_string fmt ("("^s^":"^string_of_type ty^")") in
install_user_printer("print_typed_var",print_typed_var);;
(cf.
http://www.cl.cam.ac.uk/~jrh13/hol-light/HTML/install_user_printer.html)
You may want to consider updating your windows installation of HOL Light
to the latest version.
Regards,
Petros
On 03/12/2014 10:23, Asad Ahmed wrote:
> Hi
>
> I am using Hol-light on Ubuntu 13.10, I need to know the code fragment
> or whatever the method is to invoke the type printing. There is code
> fragment in tutorial available at http://www.cl.cam.ac.uk/~jrh13/hol-light/,
>
> ---For Showing type ----)
>
> let print_typed_var tm =
> let s,ty = dest_var tm in
> print_string("("^s^":"^string_of_type ty^")") in
> install_user_printer("print_typed_var",print_typed_var);;
>
> (--For deleting types -----)
>
> delete_user_printer "print_typed_var";;
>
> It works flawlessly on windows but it is not working in Ubuntu OS.
> When I run this on emacs23 shell it goes like this
>
> # let print_typed_var tm =
> let s,ty = dest_var tm in
> print_string("("^s^":"^string_of_type ty^")") in
> install_user_printer("print_typed_var",print_typed_var);;
> Characters 138-171:
> install_user_printer("print_typed_var",print_typed_var);;
> ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
> Error: This expression has type string * (term -> unit)
> but an expression was expected of type
> string * (Format.formatter -> term -> unit)
> Type term = Hol.term is not compatible with type Format.formatter
>
>
> Thanks in Advance
>
>
> ------------------------------------------------------------------------------
> Download BIRT iHub F-Type - The Free Enterprise-Grade BIRT Server
> from Actuate! Instantly Supercharge Your Business Reports and Dashboards
> with Interactivity, Sharing, Native Excel Exports, App Integration & more
> Get technology previously reserved for billion-dollar corporations, FREE
> http://pubads.g.doubleclick.net/gampad/clk?id=164703151&iu=/4140/ostg.clktrk
>
>
>
> _______________________________________________
> hol-info mailing list
> hol-info@lists.sourceforge.net
> https://lists.sourceforge.net/lists/listinfo/hol-info
>
--
The University of Edinburgh is a charitable body, registered in
Scotland, with registration number SC005336.
------------------------------------------------------------------------------
Download BIRT iHub F-Type - The Free Enterprise-Grade BIRT Server
from Actuate! Instantly Supercharge Your Business Reports and Dashboards
with Interactivity, Sharing, Native Excel Exports, App Integration & more
Get technology previously reserved for billion-dollar corporations, FREE
http://pubads.g.doubleclick.net/gampad/clk?id=164703151&iu=/4140/ostg.clktrk
_______________________________________________
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info
