Hi Asad,
This is an intended design feature of HOL Light. Unique
numerically-named type variables are created as part of parsing in term
quotations, for term/constants that have undetermined types.
So, for example, if you entered the term quotation `x`, then the parser
wouldn't know which type is intended for "x", and so gives it a unique
type variable, which your printer would show as:
`x:?1143114`
whereas if you entered `x:A`, then the type of "x" is determined, and
your printer would print as:
`x:A`
Mark.
On 16/05/2016 07:38, Asad Ahmed wrote:
> Hi everybody,
> I am working on the VirtualBox 4.02/Ubuntu 12.04 LTS, windows 10 as
> guest OS. I installed the HOL Light following the isntruction on link:
>
> https://bitbucket.org/akrauss/hol-light-workbench
>
> It uses Ocaml version 3.12.1/camlp5-5.15, a slight modification in the
> setup script for downloading the Hol Light from
>
> git clone https://github.com/jrh13/hol-light.git
>
> I use following code fregment for showing types:
>
> 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);;
>
> When I upload the "Multivariate/make_complex.ml" or simply some other
> theory (let us say "Multivariate/topology.ml"), and want to know about
> the types I come up with datatypes of numerical attributes, e.g,
>
> # TENDSTO_REAL;;
> val it : thm =
> |- ((s:?1143113->real) ---> (l:real)) =
> (lift o (s:?1143113->real) --> lift (l:real))
> I have emacs23.
>
> Thanks in advance
>
> ------------------------------------------------------------------------------
> Mobile security can be enabling, not merely restricting. Employees who
> bring their own devices (BYOD) to work are irked by the imposition of MDM
> restrictions. Mobile Device Manager Plus allows you to control only the
> apps on BYO-devices by containerizing them, leaving personal data untouched!
> https://ad.doubleclick.net/ddm/clk/304595813;131938128;j
> _______________________________________________
> hol-info mailing list
> [email protected]
> https://lists.sourceforge.net/lists/listinfo/hol-info
------------------------------------------------------------------------------
Mobile security can be enabling, not merely restricting. Employees who
bring their own devices (BYOD) to work are irked by the imposition of MDM
restrictions. Mobile Device Manager Plus allows you to control only the
apps on BYO-devices by containerizing them, leaving personal data untouched!
https://ad.doubleclick.net/ddm/clk/304595813;131938128;j
_______________________________________________
hol-info mailing list
[email protected]
https://lists.sourceforge.net/lists/listinfo/hol-info
