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 ------------------------------------------------------------------------------ Master HTML5, CSS3, ASP.NET, MVC, AJAX, Knockout.js, Web API and much more. Get web development skills now with LearnDevNow - 350+ hours of step-by-step video tutorials by Microsoft MVPs and experts. SALE $99.99 this month only -- learn more at: http://p.sf.net/sfu/learnmore_122812 _______________________________________________ hol-info mailing list hol-info@lists.sourceforge.net https://lists.sourceforge.net/lists/listinfo/hol-info
