[opentheory-users] the Unwanted namespace

[Ramana Kumar]

The treatment of HOL4 numerals is currently "do nothing; log them as is".
(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.)
There's no post-processing to force theories to only depend on things in
base.
And I'm not sure there should be, but we can discuss it (maybe in a
different email thread).
The solution I have in mind is to use a compatibility package between base
and llist.
This was described vaguely before, e.g.
http://www.gilith.com/opentheory/mailing-list/2011-September/000119.html.

On Fri, Jan 20, 2012 at 5:53 AM, Michael Norrish <
Michael.Norrish at nicta.com.au> wrote:

> On 20/01/12 04:26, Ramana Kumar wrote:
> >
> http://opentheory.gilith.com/opentheory/packages/lazy-list-0.3/lazy-list-0.3.html
>
> I'm confused by the fact that the HTML page says that it depends on
> assumptions about
>
> Number.Numeral.bit2
>
> Shouldn't bit2 terms have been eliminated by the treatment of HOL4
> numerals?
>
> Certainly,
>
>
> http://opentheory.gilith.com/opentheory/packages/natural-numeral-1.8/natural-numeral-1.8.html
>
> only talks about bit0 and bit1.
>

> 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.)
>
> Michael
>
>
> _______________________________________________
> opentheory-users mailing list
> opentheory-users at gilith.com
> http://www.gilith.com/opentheory/mailing-list
>
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://www.gilith.com/opentheory/mailing-list/attachments/20120120/e0ed2aaa/attachment-0001.htm>