Re: [Hol-info] Learning HOL Light

[Bill R. <ri...@ma...>]

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