Thanks, Mark! Your precedence list explains my code. Why don't we try to
prove your precedence order is correct for HOL Light. Don't we just have to
understand parser.ml? I just realized I don't need type annotations if use
tactics:
let CartesianProduct = new_definition
`! X Y. X times Y = {x,y | x IN X /\ y IN Y}`;;
let IN_CartesianProduct = prove
(`! X Y x y. x,y IN X times Y <=> x IN X /\ y IN Y`,
REWRITE_TAC[IN_ELIM_THM; CartesianProduct] THEN MESON_TAC[PAIR_EQ]);;
However, that doesn't work in miz3!!! I get the error #6 underspecified types
hol with
let IN_CartesianProduct = thm `;
! X Y x y.
x,y IN X times Y <=> x IN X /\ y IN Y
by CartesianProduct, SET_RULE, PAIR_EQ`;;
So miz3 is doing something funny. Milner type inference surely tells us that
no type annotations were needed above. Well, that's fine, I don't mind feeding
miz3 extra type annotations. I suppose it helps readability. Here's a place
where my type inference intuition doesn't work, and I get the error
Exception: Failure "typechecking error (initial type assignment)":
parse_as_infix("-bb-->",(13,"right"));;
let FunctionbbSpace = new_definition
`! s t. s -bb--> t = {f | (! x. x IN s ==> f x IN t) /\
! x. x NOTIN s ==> f x = @y. T}`;;
HOL Light seems to insist on the type annotation f: A->B. But I can't see why.
A and B just mean arbitrary types. The sub-term x IN s shows that s has type
A->bool and x has type A, for some type A. and the sub-term f x IN t shows
that t has type B->bool and f x has type B, for some type B. Thus f has type
A->B. What am I missing?
--
Best,
Bill
------------------------------------------------------------------------------
LogMeIn Rescue: Anywhere, Anytime Remote support for IT. Free Trial
Remotely access PCs and mobile devices and provide instant support
Improve your efficiency, and focus on delivering more value-add services
Discover what IT Professionals Know. Rescue delivers
http://p.sf.net/sfu/logmein_12329d2d
_______________________________________________
hol-info mailing list
[email protected]
https://lists.sourceforge.net/lists/listinfo/hol-info
