[opentheory-users] the Unwanted namespace

[Ramana Kumar]

I've uploaded a much smaller (~2000 lines) gzipped article to
cam.xrchz.net/Unwanted.art.gz which fails with a similar error:

FATAL ERROR: opentheory failed:
in Article.fromTextFile:
error in file "Unwanted.art" around line 1769:
eqMp
313
def
while executing eqMp command:
  stack =
    [|- Unwanted.id x <=> let x <- x in F,
     |- (x <=> let x <- x in F) <=> x <=> F,
     |- (x <=> F) <=> (x <=> F) <=> T, x,
     |- (!x. x <=> F) ==> let x <- x in x <=> F,
     |- (let x <- x in x <=> F) <=> x <=> F, [[], [[x, T]]], |- (~) = (~),
     |- (~T <=> ~F) <=> ~T <=> T, |- (<=>) (T <=> F) = (<=>) (T <=> F),
     |- (<=>) = (<=>), |- Unwanted.id = \x. F]
in ObjectProv.mkEqMp:
in Thm.eqMp:
terms not alpha-equivalent:
     Unwanted.id x <=> let x <- x in F
  vs x <=> let x <- x in F
different term structure at path 01 subterms: Unwanted.id x vs x

However, in this case I would want processing to fail somewhere
(perhaps not like this), because I think otherwise the article's
exports would include |- T = F (and it would have consistent imports).
Perhaps the same safeguard (if that is indeed what I'm running into
here) is preventing my original article from being read, and so I'm
not using Unwanted.id correctly there somehow..?

On Fri, Oct 7, 2011 at 10:05 AM, Ramana Kumar <ramana.kumar at gmail.com> wrote:
> 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
>>
>