[opentheory-users] assumption refuses to be satisfied

[Joe Leslie-Hurd]

Hi Ramana,

Your theory file looks fine to me - it must be the case that th1 in
article art1.art and art2.art are subtly different. I recently added a
--show-types option to the opentheory tool to make it easier to check
types, perhaps this will reveal some differences?

If not I would be happy to take a look at art1.art and art2.art to see
if I can spot something (and check you have not tickled a bug in the
infrastructure).

Cheers,

Joe

On Sun, Nov 1, 2015 at 3:53 PM, 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?
>
> _______________________________________________
> opentheory-users mailing list
> opentheory-users at gilith.com
> http://www.gilith.com/opentheory/mailing-list
>