<div dir="ltr">Hi Rob,<div><br></div><div>The derived syntax in OpenTheory is rather ad-hoc: I just hard-coded some common mathematical syntax such as numerals, pairs and sets which is triggered by specific names in the OpenTheory namespace.</div>
<div><br></div><div>When exporting HOL Light theories to the OpenTheory library, one of the more involved things I had to do is remove as many HOL Light-specific tags as possible. So for example, the NUMERAL tag is easily removed, and OpenTheory numerals are instead recognized by sequences of bit0 and bit1 functions terminated by natural number zero.</div>
<div><br></div><div>The OpenTheory version of GSPEC is called fromPredicate, and you can see the standard library renamings in the OpenTheory fork of HOL Light in the file</div><div><br></div><div>opentheory/stdlib/<a href="http://stdlib.int">stdlib.int</a></div>
<div><br></div><div>This is how sets are recognized for printing purposes (assuming that the term argument to fromPredicate has the right shape).</div><div><br></div><div>Finally, I'm rather pleased by my scheme for recognizing let expressions, although it sounds like it might be causing you problems displaying your theory. Lets are simply terms that can be beta-reduced, so</div>
<div><br></div><div>(\v. t[v]) x</div><div><br></div><div>is printed as</div><div><br></div><div>let v = x in t[v]</div><div><br></div><div>No need for any special term tags, and in all the theories I have so far encountered there are no subterms in theorems that can be beta-reduced (and thus accidentally print as let).</div>
<div><br></div><div>Hope that helps,</div><div><br></div><div>Joe</div><div><br></div><div><br></div></div><div class="gmail_extra"><br><br><div class="gmail_quote">On Fri, Nov 22, 2013 at 8:08 AM, Rob Arthan <span dir="ltr"><<a href="mailto:rda@lemma-one.com" target="_blank">rda@lemma-one.com</a>></span> wrote:<br>
<blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"><div style="word-wrap:break-word">What is the status of things like let-terms and set comprehensions in the Gilith Open Theory Repo. I can't see the definitions of the magic constants that are used to represent these things (LET and GSPEC in HOL Light and HOL4)? A peculiar sequence of complicated assumptions involving let builds up in the HTML listings.<div>
<br></div><div>Regards,</div><div><br></div><div>Rob.</div></div><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" target="_blank">http://www.gilith.com/opentheory/mailing-list</a><br>
<br></blockquote></div><br></div>