<div dir="ltr">I think the problem may be that I have been reading two occurrences of th1 as the same when in fact they may be at different types (the types are not displayed).<br></div><div class="gmail_extra"><br><div class="gmail_quote">On 2 November 2015 at 10:53, Ramana Kumar <span dir="ltr"><<a href="mailto:ramana@member.fsf.org" target="_blank">ramana@member.fsf.org</a>></span> wrote:<br><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"><div dir="ltr"><div>I am having trouble constructing an OpenTheory package. Perhaps I have misunderstood the package specification language.<br><br></div><div>This is my situation. (I have omitted some details for the moment, but I can provide the actual article files etc. if necessary.)<br><br></div><div>I have two articles, art1.art and art2.art.<br><br></div><div>I can run opentheory info on each of them to see what they assume and what they prove.<br><br></div><div>opentheory info art1.art:<br></div><div>2 external type operators: ...<br></div><div>9 external constants: ...<br></div><div>6 assumptions: ... [all of these are in base]<br></div><div>2 theorems: th1, th2<br></div><div><br></div><div>opentheory info art2.art:<br></div><div>2 external type operators: ...<br></div><div>17 external constants: ...<br></div><div>27 assumptions: th1, th2, [all the rest are in base]<br></div><div>4 defined constants: ...<br></div><div>41 theorems: ...<br><br></div><div>(th1 and th2 do not mention any of the defined constants.)<br><br></div><div>Now, I make the following package, pkg.thy.<br></div><div>requires: base<br>a {<br></div><div>article: "art1.art"<br>}<br></div><div>main {<br></div><div>import: a<br></div><div>article: "art2.art"<br>}<br><br></div><div>opentheory info pkg.thy:<br></div><div>2 external type operators: ...<br></div><div>17 external constants: ...<br></div><div>26 satisfied assumptions: hidden<br></div><div>1 unsatisfied assumption: th1<br></div><div>4 defined constants: ...<br></div><div>41 theorems: ...<br><br></div><div>Why is th1 still unsatisfied? I expected no unsatisfied assumptions.<br></div><div><br></div><div>What could be going wrong?<br></div></div>
</blockquote></div><br></div>