[opentheory-users] the Unwanted namespace

[Ramana Kumar]

Thanks for making it quicker :)

Now, the only place where Unwanted.id seems not to be erased is in an
apparent axiom required by my article.
Can you confirm that the article is actually trying to define Unwanted.id?
I generated the article from a HOL4 theory that I don't think should
be defining anything mapped to Unwanted.id, so I'm a bit confused
about that at the moment...

On Tue, Dec 6, 2011 at 4:58 AM, Joe Hurd <joe at gilith.com> wrote:
> Hi Ramana,
>
> I fixed a performance bug in the proof rewriting, and your example
> goes through pretty quickly now (see below). The fix is both pushed
> and released in the latest version of the opentheory tool.
>
> Cheers,
>
> Joe
>
> ________________________________________________________________
>
> dimholt:~/dev/opentheory$ gzcat ~/Desktop/ll.art.gz | time
> bin/mlton/opentheory info --inference article:-
> WARNING: 38 objects left on the stack by -
> WARNING: 473,658 objects left in the dictionary by -
> Primitive inferences:
> eqMp ............ 150,377
> deductAntisym ... 129,584
> subst ............ 76,065
> appThm ........... 20,748
> assume ........... 18,086
> refl .............. 9,363
> betaConv .......... 7,461
> absThm ............ 4,564
> axiom ............... 193
> defineConst .......... 25
> defineTypeOp .......... 1
> Total ........... 416,467
>       24.40 real
>       15.30 user
>         9.07 sys
>
> dimholt:~/dev/opentheory$ time bin/mlton/opentheory info --inference
> foo.art Primitive inferences:
> eqMp ............. 68,100
> subst ............ 56,228
> deductAntisym .... 51,689
> appThm ........... 17,378
> betaConv .......... 6,866
> refl .............. 6,325
> absThm ............ 4,267
> assume ............ 1,608
> axiom ............... 190
> defineConst .......... 26
> defineTypeOp .......... 1
> Total ........... 212,678
>
> real    0m5.289s
> user    0m5.027s
> sys     0m0.256s
>
> _______________________________________________
> opentheory-users mailing list
> opentheory-users at gilith.com
> http://www.gilith.com/opentheory/mailing-list