Hi,
| I use ocaml 3.09.3 and hol light 2.20. After entering #use "hol.ml";; in
| ocaml toplevel I'd like to write some code which use module Map from the
| ocaml standard library. So I entered #use "map.ml";; but i got this error:
This arises because HOL Light modifies the case conventions used by OCaml
to distinguish between ordinary identifiers and special ones like module
names. It's unfortunate to have to do this, but the use of uppercase names
in HOL is well-established. The HOL Light convention is that the "special"
names are those that begin with an uppercase letter and then continue with
a lowercase letter, so "S" doesn't qualify any more, though a lot of the
usual OCaml modules will work. Some options are:
1. Disable the special parsing with "unset_jrh_lexer". You should be
able to accept normal OCaml then. To go back again to HOL Light
style, do "set_jrh_lexer".
2. Use a version of the standard OCaml library that edits out awkward
identifiers like this "S".
3. Consider using HOL Light's own built-in type "('a,'b)func" for maps.
These are a bit different from OCaml's, but in some ways more
straightforward: just use them polymorphically and compare them for
equality with "=". Try the following for more information:
help "|->"
John.
------------------------------------------------------------------------------
Crystal Reports - New Free Runtime and 30 Day Trial
Check out the new simplified licensing option that enables unlimited
royalty-free distribution of the report engine for externally facing
server and web deployment.
http://p.sf.net/sfu/businessobjects
_______________________________________________
hol-info mailing list
[email protected]
https://lists.sourceforge.net/lists/listinfo/hol-info
