[nogin] Added expand_all to mp.run top_lop_ Mon Sep 19 03:45:29 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2002-12/2005-09-19-03-45-29-934920000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2002-12/2005-09-19-03-45-29-934920000-PDT.html [yegor] Meta conversions are eliminated from code._ Mon Sep 19 03:45:30 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2002-12/2005-09-19-03-45-30-292205000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2002-12/2005-09-19-03-45-30-292205000-PDT.html [yegor] arithT is ready at first glance._ Mon Sep 19 03:45:32 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2002-12/2005-09-19-03-45-32-122667000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2002-12/2005-09-19-03-45-32-122667000-PDT.html [yegor] Some code clean up._ Mon Sep 19 03:46:01 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2002-12/2005-09-19-03-46-01-722542000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2002-12/2005-09-19-03-46-01-722542000-PDT.html [nogin] _ For some reason hash table resize used the folrmula_ Mon Sep 19 03:46:08 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2002-12/2005-09-19-03-46-08-193142000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2002-12/2005-09-19-03-46-08-193142000-PDT.html [nogin] _ Added proper intro_typeinf annotations on a number of _wf theorems._ Mon Sep 19 03:46:12 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2002-12/2005-09-19-03-46-12-476662000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2002-12/2005-09-19-03-46-12-476662000-PDT.html [nogin] Proved rev_wf_ Mon Sep 19 03:46:17 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2002-12/2005-09-19-03-46-17-963739000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2002-12/2005-09-19-03-46-17-963739000-PDT.html [yegor] cases, when reduceC actually increases the size of the term, are removed from reduce resource._ Mon Sep 19 03:46:22 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2002-12/2005-09-19-03-46-22-973618000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2002-12/2005-09-19-03-46-22-973618000-PDT.html [nogin] Fixing the problem found by Yegor__ Mon Sep 19 03:46:23 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2002-12/2005-09-19-03-46-23-343148000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2002-12/2005-09-19-03-46-23-343148000-PDT.html [yegor] Fixing the damage caused be reducing reduce_resource _now some things should be told explicitely__ Mon Sep 19 03:46:25 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2002-12/2005-09-19-03-46-25-251600000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2002-12/2005-09-19-03-46-25-251600000-PDT.html [yegor] Some addition reduce_rules. Cancelation of bnot_bnot___ added to itt_bool also_ Mon Sep 19 03:46:28 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2002-12/2005-09-19-03-46-28-245630000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2002-12/2005-09-19-03-46-28-245630000-PDT.html [nogin] Proved a few simple rules._ Mon Sep 19 03:46:29 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2002-12/2005-09-19-03-46-29-465404000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2002-12/2005-09-19-03-46-29-465404000-PDT.html [nogin] Extended the proof of nth_wf a little to provide examples to Yegor._ Mon Sep 19 03:46:56 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2002-12/2005-09-19-03-46-56-020197000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2002-12/2005-09-19-03-46-56-020197000-PDT.html [nogin] Print out the number of nodes when doing status[_all]. Also, include those_ Mon Sep 19 03:46:59 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2002-12/2005-09-19-03-46-59-189223000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2002-12/2005-09-19-03-46-59-189223000-PDT.html [nogin] Minor fix._ Mon Sep 19 03:46:59 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2002-12/2005-09-19-03-46-59-727070000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2002-12/2005-09-19-03-46-59-727070000-PDT.html [nogin] Argh, another minor fix._ Mon Sep 19 03:47:00 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2002-12/2005-09-19-03-47-00-072947000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2002-12/2005-09-19-03-47-00-072947000-PDT.html [nogin] Fixing bug _26._ Mon Sep 19 03:47:00 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2002-12/2005-09-19-03-47-00-418339000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2002-12/2005-09-19-03-47-00-418339000-PDT.html [nogin] _ We used to generase resource _bookmarks_ _checkpoints_ for all_ Mon Sep 19 03:47:00 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2002-12/2005-09-19-03-47-00-856274000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2002-12/2005-09-19-03-47-00-856274000-PDT.html [nogin] Minor clarification._ Mon Sep 19 03:47:02 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2002-12/2005-09-19-03-47-02-508700000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2002-12/2005-09-19-03-47-02-508700000-PDT.html