<div dir="ltr">Hi Rob,<div><br></div><div class="gmail_extra"><div class="gmail_quote"><blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left-width:1px;border-left-color:rgb(204,204,204);border-left-style:solid;padding-left:1ex">
<div style="word-wrap:break-word"><div><div class=""><blockquote type="cite"><div dir="ltr"><div class="gmail_extra"><div class="gmail_quote"><div>The above command takes about 45 seconds to complete on my machine and the resulting thm.art is 6Mb in size.</div>
</div></div></div></blockquote><br></div></div><div>This looks like it will be useful when you have sorted out the glitches in the package names.</div></div></blockquote><div><br></div><div>Over the weekend I made a new release of the standard theory library</div>
<div><br></div><div><a href="http://opentheory.gilith.com/?pkg=base-1.158">http://opentheory.gilith.com/?pkg=base-1.158</a><br></div><div><br></div><div>so this command now works as intended to extract the "pure theorem" content.</div>
<div><br></div><blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left-width:1px;border-left-color:rgb(204,204,204);border-left-style:solid;padding-left:1ex"><div style="word-wrap:break-word"><div>I have now imported the packages, bool, function, unit, pair, natural and option. The process is a bit clunky, but is perfectly workable. The Repo website is extremely helpful. So I would say my issues with designing a reader are resolved.</div>
</div></blockquote><div><br></div><div>Excellent, very glad to hear it.</div><div><br></div><blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left-width:1px;border-left-color:rgb(204,204,204);border-left-style:solid;padding-left:1ex">
<div style="word-wrap:break-word"><div>One query: is the case constant in the option package really meant to be called Data.case.none.some? That doesn’t seem to agree with the web page for the package.</div></div></blockquote>
<div><br></div><div>Case constants are treated specially by the opentheory printer, to support pretty-printing of case expressions. You can see some example case expressions in the parser theory:</div><div><br></div><div>
<a href="http://opentheory.gilith.com/opentheory/packages/parser-1.100/parser-1.100.html">http://opentheory.gilith.com/opentheory/packages/parser-1.100/parser-1.100.html</a><br></div><div><br></div><div>It's perhaps ugly, but to avoid the need for symbol tables the OpenTheory convention is to append the name of the constructors to the case constant, hence Data.Option.case.none.some. This makes it possible to pretty-print</div>
<div><br></div><div>case.none.some x (\a. y a) z</div><div><br></div><div>as</div><div><br></div><div>case z of none -> x | some a -> y a</div><div><br></div><div>You can see the true name and type of the case constant by hovering over it in the package document (the same goes for all variables and constants).</div>
<div><br></div><div>Cheers,</div><div><br></div><div>Joe</div><div><br></div></div></div></div>