On 12/01/11 12:16 AM, Ramana Kumar wrote: > Are HOL4 theories allowed to have constants with the same name but > different types?
No. > In other words, is a HOL4 constant uniquely identified by the Thy and > Name fields in the record returned by dest_thy_const, or does the Type > field matter too? The former. > Same question for type operators: is the Args field in the record > returned by dest_thy_type relevant when identifying the type operator? The Args field is not relevant; the analogous question would actually be whether or not the arity (length of Args) of the operator was relevant. In summary: The thy-name combination uniquely identifies HOL constants and type operators. The Type.op_arity and Term.prim_mk_const functions would not make sense otherwise. Michael ------------------------------------------------------------------------------ Protect Your Site and Customers from Malware Attacks Learn about various malware tactics and how to avoid them. Understand malware threats, the impact they can have on your business, and how you can protect your company and customers by using code signing. http://p.sf.net/sfu/oracle-sfdevnl _______________________________________________ hol-info mailing list [email protected] https://lists.sourceforge.net/lists/listinfo/hol-info
