Thanks for responding! Vincent's idea worked. I have new question:
(* Paste in these 2 commands:
hol_light> ocaml
#use "hol.ml";;
pasting this in gives an error message *)
new_type("element",0);;
new_constant("prod",`:element->element->element`);;
new_constant("elt_inv",`:element->element`);;
new_constant("unit",`:element`);;
parse_as_infix("prod",(20, "right"));;
let A1 = new_axiom
`!x y z. (x prod y) prod z = x prod (y prod z)`;;
let left_unit = new_axiom
`!x . unit prod x = x`;;
let left_inv = new_axiom
`!x . elt_inv(x) prod x = unit`;;
(*
I think it's quite interesting that HOL Light left out parentheses
val left_inv : thm = |- !x. elt_inv x prod x = unit
This does not: *)
parse_as_prefix "elt_inv";;
let left_inv = new_axiom
`!x . (inv x) prod x = unit`;;
(* I get the usual "typechecking error (initial type assignment)". *)
Vincent, thanks for explaining that inv was already defined:
type_of `inv`;;
val it : hol_type = `:real->real`
I'm an HOL Light newbie. What should I have read so that I would have
known that? Neither prefixes();; nor infixes();; lists `inv'.
Should I just make a habit of evaluating things like
type_of `elt_inv`;;
to see that I'm inventing a new type?
Toal, your fix
let left_inv = new_axiom
`!x . (inv x) prod x = unit`;;
did not work if we just substitute your axiom for mine. Same error:
Exception: Failure "typechecking error (initial type assignment)".
--
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
[email protected]
https://lists.sourceforge.net/lists/listinfo/hol-info
