Re: [Hol-info] Learning HOL Light

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

   Just because you don't write the A doesn't mean it isn't there. And
   if you'll still need to be careful if there's an A in context,
   whether you write it explicitly or not, although hopefully type
   inference will pick another type variable for you if there's
   already an A around (e.g. B).

Thanks, Ramana!  I think type inference always behaves that way. I mean, I've always assumed it did, and in my limited experience, it does. 

   You seem to have missed the point that HOL Omega already has type
   quantification. If you want type quantification, you should
   definitely be using it.

I'm sold on HOL Light, which Tom Hales particularly recommended in his Notices AMS article "Formal Proof", and largely because of John Harrison's interest in formalizing pure math.  

-- 
Best,
Bill