[opentheory-users] Debugging a failing trans
joe at leslie-hurd.com
Thu Apr 27 19:43:24 UTC 2017
If you compile the development version of the opentheory tool
and use it to process the article file, you get a lot more error
information including these last few lines:
different constants at path 10110 subterms: HOL4.min.@ vs HOL4.min.
different constants: HOL4.min.@ vs HOL4.min.
different constant names
So it looks like there are different constants at subterm path 10110.
On Wed, Apr 26, 2017 at 2:22 PM, Ramana Kumar <ramana at member.fsf.org> wrote:
> Hi OpenTheory list,
> I am trying to find out more about why an article file I generated causes
> opentheory to fail. It prints this error:
> FATAL ERROR: opentheory failed:
> error in file "Test.art" around line 37270:
> while executing trans command:
> terms not alpha-equivalent
> So obviously the trans command failed. But my attempts to figure out which
> theorems are being "trans"ed at that point (I made the article generator add
> comments) turned up theorems that looked OK. So, is it possible to ask the
> opentheory tool to give more information about the failing theorems? Can it
> print them out?
> The failing article can be found (for now) at
> opentheory-users mailing list
> opentheory-users at gilith.com
More information about the opentheory-users