Thanks, Michael! As you see, I haven't read the HOL4 Description manual carefully yet. I should, because I think it's quite possible you might have some good explanations not in the HOL Light dox. Since HOL4 ports HOL Light's finite cartesian products, maybe you can explain it! As you write on p 84 of Description:
dimindex(’b) is the cardinality of univ(:’b) That's easier to read that the HOL Light cart.ml code let dimindex = new_definition `dimindex(s:A->bool) = if FINITE(:A) then CARD(:A) else 1`;; But it doesn't explain to me how to prove these theorems so necessary for the vector types real^2 and real^3: # DIMINDEX_2;; val it : thm = |- dimindex (:2) = 2 # DIMINDEX_3;; val it : thm = |- dimindex (:3) = 3 And as Rob says that eventually we should modify HOL to allow type quantification, 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. -- Best, Bill ------------------------------------------------------------------------------ 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 [email protected] https://lists.sourceforge.net/lists/listinfo/hol-info
