Hi Mike, | Anyone know what recspace is (see question below)? I've not come | across it before.
This type is used internally in HOL Light's type definition package. Roughly, ":(A)recspace" is a type large enough to hold any finitely branching recursive type built up from starting types that can be injected into ":A". All types defined by "define_type" are carved out of a type of the form, at least in HOL Light. It's defined in the HOL Light source file "ind-types.ml". I believe the HOL4 type definition package uses, or at least used, the same code: src/datatype/ind_typeScript.sml src/datatype/ind_types.sml John. ------------------------------------------------------------------------- Check out the new SourceForge.net Marketplace. It's the best place to buy or sell services for just about anything Open Source. http://sourceforge.net/services/buy/index.php _______________________________________________ hol-info mailing list [email protected] https://lists.sourceforge.net/lists/listinfo/hol-info
