<div dir="ltr"><div class="gmail_extra"><div class="gmail_quote">On 9 August 2015 at 19:02, Günter Rote <span dir="ltr"><<a href="mailto:rote@inf.fu-berlin.de" target="_blank">rote@inf.fu-berlin.de</a>></span> wrote:<br><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">Am 08.08.2015 um 03:16 schrieb Joe Leslie-Hurd:<br>
> Thanks for the clarification, I have added a note to defineConst and<br>
> defineTypeOp to spell this out:<br>
><br>
> <a href="http://www.gilith.com/research/opentheory/article.html#defineConstCommand" rel="noreferrer" target="_blank">http://www.gilith.com/research/opentheory/article.html#defineConstCommand</a><br>
> <a href="http://www.gilith.com/research/opentheory/article.html#defineTypeOpCommand" rel="noreferrer" target="_blank">http://www.gilith.com/research/opentheory/article.html#defineTypeOpCommand</a><br>
<br>
Thanks. But what is the *principal* type of the new constant?<br></blockquote><div><br></div><div>HOL constants are polymorphic. But the type of every instance of a particular constant is a type instance of one particular type. That one type is the principal type of the constant.<br></div><div> </div><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">
(And maybe you want to update defineConstList as well?)<br></blockquote><div><br></div><div>Yes, I think an analogous note would make sense.<br></div><div> </div><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">
<br>
Am 15.01.2011 um 03:16 schrieb Joe Leslie-Hurd:<br>
<a href="http://www.gilith.com/opentheory/mailing-list/2011-January/000080.html" rel="noreferrer" target="_blank">http://www.gilith.com/opentheory/mailing-list/2011-January/000080.html</a><br>
>> Also, it's not clear whether a "new constant" with the same name as<br>
>> a previously defined constant is allowed. I presume so.<br>
><br>
> This is left to the system, which must be careful to disallow<br>
><br>
1. define `c = T`<br>
2. define `c = F`<br>
3. prove `T = F`<br>
><br>
> I believe all of the HOL theorem provers maintain a symbol table of<br>
> constants, and will not allow redefinitions with the same name. The<br>
> logical kernel of the opentheory tool stores the definition with the<br>
> constant, so will happily allow redefinitions with the same name<br>
> (because the two "c" constants above will be treated as different<br>
> constants).<br>
<br>
This puzzles me.<br>
If I now create another "instance" of a constant with name c<br>
(and type bool) by a const+constTerm command, to which<br>
constant from among definitions 1 or 2 (if any) does it<br>
refer to?</blockquote><div><br></div><div>Neither. The only way to get the constants from the definitions in 1 and 2 is as the objects returned by the definition commands.<br></div><div> </div><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"> (More specifically, to which c will it be<br>
alpha-equivalent, when this is for example tested in<br>
the course of eqMP?)<br></blockquote><div><br></div><div>(neither)<br></div><div> </div><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">
And does the answer change for a constant c that was<br>
"created" before definitions 1 and 2?<br></blockquote><div><br></div><div>No. (I'm not 100% confident of these three answers; Joe will know best.)<br></div><div> </div><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">
<br>
best regards : Günter<br>
<br>
<br>_______________________________________________<br>
opentheory-users mailing list<br>
<a href="mailto:opentheory-users@gilith.com">opentheory-users@gilith.com</a><br>
<a href="http://www.gilith.com/opentheory/mailing-list" rel="noreferrer" target="_blank">http://www.gilith.com/opentheory/mailing-list</a><br>
<br></blockquote></div><br></div></div>