It should be noted that this uniqueness applies to the internal, canonical name of a constant in a given theory (i.e. the name returned by 'dest_thy_const'), as opposed to names for a constant that can appear in term quotations. In HOL4 term quotations, constants can be aliased, and these aliases can be overloaded, even for constants of the same theory.
Mark. on 11/1/11 9:41 PM, Michael Norrish <[email protected]> wrote: > 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 > > _______________________________________________ > hol-info mailing list > [email protected] > https://lists.sourceforge.net/lists/listinfo/hol-info > > > ------------------------------------------------------------------------------ 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
