Hi Konrad, | I have a student wanting to translate Michael Norrish's | DPLL example to HOL-Light. Part of that involves | replacing HOL-4's use of the Binarymap structure | with the appropriate thing in HOL-Light. It seemed | like instantiating OCaml's Map functor was the right | approach,
That might indeed be the most natural/efficient, though you might also consider the type of finite partial functions that is in HOL Light's "lib.ml" file. This may be less efficient than the OCaml map structure but it's not bad, and does have two nice features: * It's simply polymorphic and you don't need to instantiate it for various types * The type is canonical so you can compare two FPFs just by using the ordinary OCaml equality. To find out more about the interface, you might start by help "|->";; But anyway, back to the real question: | module OrderedTerm = | struct | type t = term | let compare x y = (Pervasives.compare: term -> term -> int) x y | end;; | | was rejected as being badly formed. However, the only slightly | different The problem is that in order to support the HOL tradition of using uppercase identifiers like REWRITE_TAC, the HOL Light setup changes the OCaml identifier case distinctions a bit. Generally, this is quite close to the conventions OCaml programmers actually use, but not always. By default, OCaml treats as "special" (type constructor, module etc.) any identifier that starts with an uppercase letter. In the HOL Light variant, it must start with an uppercase letter *and* otherwise consist entirely of lowercase letters. Thus "OrderedTerm" doesn't qualify as special. But you could use "Orderedterm" instead. John. ------------------------------------------------------------------------- This SF.net email is sponsored by the 2008 JavaOne(SM) Conference Don't miss this year's exciting event. There's still time to save $100. Use priority code J8TL2D2. http://ad.doubleclick.net/clk;198757673;13503038;p?http://java.sun.com/javaone _______________________________________________ hol-info mailing list [email protected] https://lists.sourceforge.net/lists/listinfo/hol-info
