[opentheory-users] the Unwanted namespace

[Michael Norrish]

On 20/01/12 04:26, Ramana Kumar wrote:
> To my mild surprise, logging the proof of the point-free theorem
> worked. That is, if I make sure the theorem with an unapplied
> Unwanted.id is logged with a proof (while logging the lazy list
> theory), then process the resulting article with opentheory, the
> resulting package doesn't define Unwanted.id and doesn't require any
> axioms. I've uploaded the new version of the lazy list package, which
> now appears to define and prove just the right things.
> 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

-------------- next part --------------
A non-text attachment was scrubbed...
Name: signature.asc
Type: application/pgp-signature
Size: 554 bytes
Desc: OpenPGP digital signature
URL: <http://www.gilith.com/opentheory/mailing-list/attachments/20120120/4af6f9fb/attachment.pgp>