[opentheory-users] the Unwanted namespace

[Ramana Kumar]

it occurs to me that it might be a types problem - would the
opentheory tool require the Unwanted.id constant to be created with a
particular type?

On Fri, Oct 7, 2011 at 10:03 AM, Ramana Kumar <ramana.kumar at gmail.com> wrote:
>>> Currently the tool is failing to process an article because at
>>> some point an extra Unwanted.id means two terms that should be
>>> alpha-convertible aren't. (But I don't think it's the first occurrence
>>> of Unwanted.id in the article.)
>>
>> Is there any way of reducing your problem to a simple case that I could look at?
>>
>
> Maybe - any suggestions? In the meantime the complete (gzipped)
> article is available here http://cam.xrchz.net/llist.art.gz. Maybe
> running opentheory with some extra debugging code to see whatever it
> does to Unwanted.id tags during reading this article will be
> helpful...
>
> FYI the error I get is
>
> ...
> in ObjectProv.mkEqMp:
> in Thm.eqMp:
> terms not alpha-equivalent:
>     Number.Natural.+ (Number.Numeral.bit2 Number.Numeral.zero)
>       (Number.Numeral.bit1 Number.Numeral.zero) =
>     Number.Natural.+ (Number.Numeral.bit2 Number.Numeral.zero)
>       (Number.Numeral.bit1 Number.Numeral.zero)
>  vs Number.Natural.+ (Number.Numeral.bit2 Number.Numeral.zero)
>       (Number.Numeral.bit1 Number.Numeral.zero) =
>     Unwanted.id
>       (Number.Natural.+ (Number.Numeral.bit2 Number.Numeral.zero)
>          (Number.Numeral.bit1 Number.Numeral.zero))
> different term structure at path 10 subterms:
>     Number.Natural.+ (Number.Numeral.bit2 Number.Numeral.zero)
>  vs Unwanted.id
>