Thanks, Michael, I'll try out your cong trick. Your type_of `MAP`;; was plenty illuminating, that's how I figured out what polymorphism meant, with the Scheme analogy, but I'm confused. On p 350 of http://www.cl.cam.ac.uk/~jrh13/hol-light/reference.pdf it explains lower-case map: map : ('a -> 'b) -> 'a list -> 'b list Are you saying this is an Ocaml function, and not something we can use in HOL Light? A few pages later is MAP_EVERY : ('a -> tactic) -> 'a list -> tactic That certainly sounds like HOL Light. There is no MAP in reference.pdf. This brings up a question Colin Rowat was asking earlier: if you define various vector-related functions in HOL Light (like the maximum of a vector, or the dot product of two vectors...), how can you check if your code is working? Is there some cooperation between ML and HOL that I'm missing? Obviously HOL is coded up in ML, but are you supposed to mix freely ML and HOL code somehow?
-- Best, Bill ------------------------------------------------------------------------------ Live Security Virtual Conference Exclusive live event will cover all the ways today's security and threat landscape has changed and how IT managers can respond. Discussions will include endpoint security, mobile security and the latest in malware threats. http://www.accelacomm.com/jaw/sfrnl04242012/114/50122263/ _______________________________________________ hol-info mailing list hol-info@lists.sourceforge.net https://lists.sourceforge.net/lists/listinfo/hol-info
