[opentheory-users] Print unsatisfied assumptions

[Ramana Kumar]

Abstractly, my use-case is:
I have a package A that develops some concepts that are already in a
standard library package, B.
A is developed from scratch, but goes much further than B.
I want to present A as if it were based on B, rather than developed from
scratch.
So, I pull out the foundations from A, replace them by B, and then I want
to see what remaining foundational assumptions need to be proved manually
(starting from what is provided by B).

On 10 May 2016 at 16:08, Joe Leslie-Hurd <joe at gilith.com> wrote:

> I can't think of any way of persuading the existing opentheory tool to
> give you this functionality, except in the way you describe.
>
> I'd be happy to add the functionality to the tool, but it may take a
> little while.
>
> As a matter of curiosity, what is your use-case for this functionality?
>
> Cheers,
>
> Joe
>
> On Sun, May 8, 2016 at 7:09 PM, Ramana Kumar <ramana at member.fsf.org>
> wrote:
> > Hi,
> >
> > How can I get the unsatisfied assumptions of a theory in article format?
> >
> > I know about the info --assumptions option, but it prints _all_
> assumptions,
> > including the satisfied ones.
> >
> > The only way I have found so far to do it is to create a fake package
> that
> > imports all the required packages and print the assumptions of that. But
> > it's rather cumbersome to do so. Especially because importing the
> required
> > packages also means figuring out all their dependencies and recreating
> them
> > as blocks within the theory file in the right order.
> >
> > I know the opentheory tool knows how to calculate just the unsatisfied
> > assumptions. How can I get them out of it?
> >
> > Cheers,
> > Ramana
> >
> >
> > _______________________________________________
> > opentheory-users mailing list
> > opentheory-users at gilith.com
> > http://www.gilith.com/opentheory/mailing-list
> >
>
> _______________________________________________
> opentheory-users mailing list
> opentheory-users at gilith.com
> http://www.gilith.com/opentheory/mailing-list
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://www.gilith.com/opentheory/mailing-list/attachments/20160510/13358b51/attachment.html>