[opentheory-users] Debugging a failing trans

[Ramana Kumar]

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:
 trans
 5016
 def
 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 https://hol-theorem-prover.
org/Test.art.

Cheers,
Ramana
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://www.gilith.com/opentheory/mailing-list/attachments/20170427/8e520809/attachment.html>