<div class="gmail_quote">The treatment of HOL4 numerals is currently "do nothing; log them as is".<br>(Similar comment for Relation.transitive, although that might be a case
of giving a constant the wrong OpenTheory name; if it's different it
should probably be HOL4.transitive or Relation.curriedTransitive or
something.)<br>There's no post-processing to force theories to only depend on things in base.<br>And I'm not sure there should be, but we can discuss it (maybe in a different email thread).<br>The solution I have in mind is to use a compatibility package between base and llist.<br>
This was described vaguely before, e.g. <a href="http://www.gilith.com/pipermail/opentheory-users/2011-September/000119.html">http://www.gilith.com/pipermail/opentheory-users/2011-September/000119.html</a>.<br><br>On Fri, Jan 20, 2012 at 5:53 AM, Michael Norrish <span dir="ltr"><<a href="mailto:Michael.Norrish@nicta.com.au">Michael.Norrish@nicta.com.au</a>></span> wrote:<br>
<blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"><div class="im">On 20/01/12 04:26, Ramana Kumar wrote:<br>
> <a href="http://opentheory.gilith.com/opentheory/packages/lazy-list-0.3/lazy-list-0.3.html" target="_blank">http://opentheory.gilith.com/opentheory/packages/lazy-list-0.3/lazy-list-0.3.html</a><br>
<br>
</div>I'm confused by the fact that the HTML page says that it depends on assumptions about<br>
<br>
Number.Numeral.bit2<br>
<br>
Shouldn't bit2 terms have been eliminated by the treatment of HOL4 numerals?<br>
<br>
Certainly,<br>
<br>
<a href="http://opentheory.gilith.com/opentheory/packages/natural-numeral-1.8/natural-numeral-1.8.html" target="_blank">http://opentheory.gilith.com/opentheory/packages/natural-numeral-1.8/natural-numeral-1.8.html</a><br>
<br>
only talks about bit0 and bit1.<br></blockquote><div></div><blockquote class="gmail_quote" style="margin:0pt 0pt 0pt 0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex">
<br>
Similarly, your llist summary talks about a Relation.transitive thing that doesn't exist. (The transitive thing in llist is derived from Scott's relations-as-sets-of-pairs, but the one in base is a curried thing.)<br>
<span class="HOEnZb"><font color="#888888"><br>
Michael<br>
<br>
</font></span><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/mailman/listinfo/opentheory-users" target="_blank">http://www.gilith.com/mailman/listinfo/opentheory-users</a><br>
<br></blockquote></div><br>