Thanks, Mark! This is very cool, and I did not know it:
Milner type inference tells us that type annotations are never needed!
And I don't need type annotations for FunctionSpace! These two results are
fine:
let FunctionSpace = new_definition
`! s t. s ---> t = {f | (! x. x IN s ==> f x IN t) /\
! x. x NOTIN s ==> f x = @y. T}`;;
let IN_FunctionSpace = prove
(`! s t f. f IN s ---> t
<=> (! x. x IN s ==> f x IN t) /\ ! x. x NOTIN s ==> f x = @y. T`,
REWRITE_TAC[IN_ELIM_THM; FunctionSpace]);;
I'm still getting the error message I got yesterday:
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}`;;
Your NOTIN suggestion made great sense, but that's not the problem, it seems,
because FunctionSpace/---> worked. I think HOL Light doesn't like my weird
infix -bb-->. HOL Light won't even take this as a function:
let FunctionddSpace = new_definition
`! s t. -dd--> s t = {f | (! x. x IN s ==> f x IN t) /\
! x. x NOTIN s ==> f x = @y. T}`;;
I get the error Exception: Noparse.
It's good practice to explicitly type-annotate your terms with any
type variables, rather than to get HOL Light to generate type
variables for you.
Perhaps I don't agree with you. Michael Norrish argued eloquently that type
inference makes HOL more expressive, more abole to formalize pure math. But
it's a good point you're making.
I don't know about miz3, but I'm guessing it doesn't allow type
variables to be generated.
Interesting suggestion! Perhaps Freek will tell us.
that's easier said than done! Parsers can be subtle things.
Yes, but it's something we're supposed to understand, nicht wahr? How do you
handle precedence in your HOL Zero? I'd guess it's similar to the way HOL
Light does precedence.
--
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
