hol-light icon indicating copy to clipboard operation
hol-light copied to clipboard

How to use Map.Make after "hol.ml"?

Open fblanqui opened this issue 2 years ago • 2 comments

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))?

fblanqui avatar Jan 16 '23 14:01 fblanqui

You can use

unset_jrh_lexer;;

to go back to normal OCaml syntax and

set_jrh_lexer;;

to reactivate CAML Light / HOL Light syntax.

maggesi avatar Jan 16 '23 16:01 maggesi

Thanks!

fblanqui avatar Jan 16 '23 18:01 fblanqui