Bill, On Jan 16, 2013, at 1:31 PM, Bill Richter <rich...@math.northwestern.edu> wrote:
> > … > And as Rob says that eventually we should modify HOL to allow type > quantification You make me sound more definite about this than I actually feel. In fact it has already been done (for HOL4) in the shape of Peter Homeier's HOL-Omega. But Peter has gone quite a bit further than I expected. > maybe we should ask if we shouldn't allow terms to show up it types, so we > could define real^3 where 3 has type num, as it normally does, rather than > being a type that somehow satisfies dimindex (:3) = 3. You are now entering the world of dependent types - where the extent of a type can depend on the value of a term. This introduces a whole new set of complications. I don't recall how far down this path HOL-Omega goes. Regards, Rob. ------------------------------------------------------------------------------ Master Java SE, Java EE, Eclipse, Spring, Hibernate, JavaScript, jQuery and much more. Keep your Java skills current with LearnJavaNow - 200+ hours of step-by-step video tutorials by Java experts. SALE $49.99 this month only -- learn more at: http://p.sf.net/sfu/learnmore_122612 _______________________________________________ hol-info mailing list hol-info@lists.sourceforge.net https://lists.sourceforge.net/lists/listinfo/hol-info
