Re: [isabelle] referring to constants that have just been defined



Florian Haftmann writes:
> Hello Michael,
 
> > It seems that using 
 
> >   Sign.intern_const
 
> > will give me the correct qualified name for the constant (I do know
> > its name after all), but I'm worried about the situation when multiple
> > constants from different theories have the same name.  What will
> > intern_const do then?
 
> > Is there a function that will give me the name of the current theory,
> > so that I can construct the fully-qualified name myself?  
 
> Context.theory_name or Sign.full_name may prove helpful. But be aware 
> that though the default naming policy is indeed "theory name + 
> unqualified name", this might be changed.
 
Thanks for that.  So it does seem as if I should use
Sign.intern_const.

In particular, what does intern_const do when there are multiple
constants of the same name in different theories?

Michael.






This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.