Harry Hull wrote: > I would like to know if the language allowed for products and > summations. (I am in the process of going through all the documentation > I can get my hands on, but I have not found anything about products and > specifically infite products).
Example of product type (called "pair"): - type_of ``(4, T)``; > val it = ``:num # bool`` : hol_type Example of sum type (called "sum"): - type_of ``INL 4``; <<HOL message: inventing new type variable names: 'a>> > val it = ``:num + 'a`` : hol_type - type_of ``INR T``; <<HOL message: inventing new type variable names: 'a>> > val it = ``:'a + bool`` : hol_type Infinite product would be dependent type, wouldn't it? HOL doesn't come with dependent types out of the box, and I haven't seen an add-on library for it. ------------------------------------------------------------------------- This SF.Net email is sponsored by the Moblin Your Move Developer's challenge Build the coolest Linux based applications with Moblin SDK & win great prizes Grand prize is a trip for two to an Open Source event anywhere in the world http://moblin-contest.org/redirect.php?banner_id=100&url=/ _______________________________________________ hol-info mailing list [email protected] https://lists.sourceforge.net/lists/listinfo/hol-info
