Hi,
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, but we weren't able to even define the
appropriate instance of OrderedType needed as
input to Map. Thus
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
module OrderedInt =
struct
type t = int
let compare x y = (Pervasives.compare:int->int->int) x y
end;;
was accepted in pure Ocaml. Is there something about
HOL-Light that disallows the above definition of OrderedTerm,
or have I bungled the syntax?
Thanks,
Konrad.
-------------------------------------------------------------------------
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
