<div dir="ltr"><div class="gmail_extra"><div class="gmail_quote">Hi Joe,<br><br>On Sat, Dec 20, 2014 at 9:09 PM, 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:0px 0px 0px 0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex"><span class="">> Show me the intermediate (i.e. unexported) theorems that arise when running<br>
> an article.<br>
<br>
</span>No, unfortunately not. The best it can do is tell you *how many*<br>
theorems are generated, by using the --inference option.<br>
<br>
Did you have any thoughts on a way to present intermediate theorems to the user?<br></blockquote><div><br></div><div>What would be useful to me is if I could search for intermediate theorems with a pattern. I'd guess you'd rather stay away from specifying parsing of such patterns. I wouldn't mind, however, writing my pattern as OpenTheory article commands for creating a term. I'd then like to get back all intermediate theorems that match.</div><div> </div><blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex">
<span class="">
> Create an article that exports a previously unexported theorem, taking an<br>
> existing article as input.<br>
<br>
</span>Also no I'm afraid.<br></blockquote><div><br></div><div>That's a pity. Would it be hard to add? Presuming we solve the problem above of specifying an intermediate theorem.<br><br>I guess for the moment I can get around this by using a custom reader that looks for the theorem I want and cuts off the article as soon as it finds it (and adds on an export). It would be nice if the opentheory tool had enough features to support this itself, but maybe it's a little outside your design goals? On the other hand, I think a good suite of powerful manipulations on OpenTheory packages for a variety of purposes would help buy-in.<br></div><div> </div><blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex">
<span class="">
> Minimise an article for what is required for a particular theorem (I think<br>
> the answer here is yes, by creating a package with the desired theorem and<br>
> then asking for an article for it to be generated...?)<br>
<br>
</span>Indeed. Suppose article foo.art exports a set of theorems containing a<br>
theorem T of interest, then you can create an article bar.art that<br>
proves T by axiom, and then run<br>
<br>
echo 'a { article: "foo.art" } main { import: a article: "bar.art" }'<br>
| opentheory info --article -o baz.art theory:-<br>
<br>
to get a minimal article baz.art proving T.<br></blockquote><div><br></div><div>Great, thanks. <br></div></div></div></div>