Are HOL4 theories allowed to have constants with the same name but different types? 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? Same question for type operators: is the Args field in the record returned by dest_thy_type relevant when identifying the type operator?
------------------------------------------------------------------------------ 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
