hol-light
hol-light copied to clipboard
How to use Map.Make after "hol.ml"?
Hello. Using ocaml.4.02.3 and campl5.6.17 I get the following problem:
#use "hol.ml";;
# module OrdInt = struct type t = int let compare = (-) end;;
Toplevel input:
# module OrdInt = struct type t = int let compare = (-) end;;
^^^^^^
Parse error: 'type' or 'rec' expected after 'module' (in [str_item])
Why can't I define modules anymore? How do I do to build maps on integers (Map.Make(OrdInt))?
You can use
unset_jrh_lexer;;
to go back to normal OCaml syntax and
set_jrh_lexer;;
to reactivate CAML Light / HOL Light syntax.
Thanks!