<div dir="ltr"><div><div><div>Abstractly, my use-case is:<br></div>I have a package A that develops some concepts that are already in a standard library package, B.<br></div><div>A is developed from scratch, but goes much further than B.<br></div>I want to present A as if it were based on B, rather than developed from scratch.<br></div>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).<br></div><div class="gmail_extra"><br><div class="gmail_quote">On 10 May 2016 at 16:08, Joe Leslie-Hurd <span dir="ltr"><<a href="mailto:joe@gilith.com" target="_blank">joe@gilith.com</a>></span> wrote:<br><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">I can't think of any way of persuading the existing opentheory tool to<br>
give you this functionality, except in the way you describe.<br>
<br>
I'd be happy to add the functionality to the tool, but it may take a<br>
little while.<br>
<br>
As a matter of curiosity, what is your use-case for this functionality?<br>
<br>
Cheers,<br>
<br>
Joe<br>
<div><div class="h5"><br>
On Sun, May 8, 2016 at 7:09 PM, Ramana Kumar <<a href="mailto:ramana@member.fsf.org">ramana@member.fsf.org</a>> wrote:<br>
> Hi,<br>
><br>
> How can I get the unsatisfied assumptions of a theory in article format?<br>
><br>
> I know about the info --assumptions option, but it prints _all_ assumptions,<br>
> including the satisfied ones.<br>
><br>
> The only way I have found so far to do it is to create a fake package that<br>
> imports all the required packages and print the assumptions of that. But<br>
> it's rather cumbersome to do so. Especially because importing the required<br>
> packages also means figuring out all their dependencies and recreating them<br>
> as blocks within the theory file in the right order.<br>
><br>
> I know the opentheory tool knows how to calculate just the unsatisfied<br>
> assumptions. How can I get them out of it?<br>
><br>
> Cheers,<br>
> Ramana<br>
><br>
><br>
</div></div>> _______________________________________________<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>
<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>
</blockquote></div><br></div>