[opentheory-users] assumption refuses to be satisfied

[Ramana Kumar]

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).

On 2 November 2015 at 10:53, Ramana Kumar <ramana at member.fsf.org> wrote:

> I am having trouble constructing an OpenTheory package. Perhaps I have
> misunderstood the package specification language.
>
> This is my situation. (I have omitted some details for the moment, but I
> can provide the actual article files etc. if necessary.)
>
> I have two articles, art1.art and art2.art.
>
> I can run opentheory info on each of them to see what they assume and what
> they prove.
>
> opentheory info art1.art:
> 2 external type operators: ...
> 9 external constants: ...
> 6 assumptions: ... [all of these are in base]
> 2 theorems: th1, th2
>
> opentheory info art2.art:
> 2 external type operators: ...
> 17 external constants: ...
> 27 assumptions: th1, th2, [all the rest are in base]
> 4 defined constants: ...
> 41 theorems: ...
>
> (th1 and th2 do not mention any of the defined constants.)
>
> Now, I make the following package, pkg.thy.
> requires: base
> a {
> article: "art1.art"
> }
> main {
> import: a
> article: "art2.art"
> }
>
> opentheory info pkg.thy:
> 2 external type operators: ...
> 17 external constants: ...
> 26 satisfied assumptions: hidden
> 1 unsatisfied assumption: th1
> 4 defined constants: ...
> 41 theorems: ...
>
> Why is th1 still unsatisfied? I expected no unsatisfied assumptions.
>
> What could be going wrong?
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://www.gilith.com/opentheory/mailing-list/attachments/20151102/1c347f23/attachment.html>