On 13/08/12 14:53, Bill Richter wrote: > That sounds great, but here I want more details: > > The types are presented in the HOL Light System box. > > Terms are the basic mathematical objects of the HOL Light system. The > syntax is based on Church’s lambda-calculus [to define functions] > > What is a type? Compared to a set, I think. What is a term?
A type is a non-empty set. A term denotes a value in a type (i.e., an element of the non-empty set denoted by the type that term has). (Simplifying slightly; the above is true as long as the type is not polymorphic.) Michael ------------------------------------------------------------------------------ Live Security Virtual Conference Exclusive live event will cover all the ways today's security and threat landscape has changed and how IT managers can respond. Discussions will include endpoint security, mobile security and the latest in malware threats. http://www.accelacomm.com/jaw/sfrnl04242012/114/50122263/ _______________________________________________ hol-info mailing list hol-info@lists.sourceforge.net https://lists.sourceforge.net/lists/listinfo/hol-info
