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
