[opentheory-users] Debugging a failing trans

Ramana Kumar ramana at member.fsf.org
Wed Apr 26 21:22:11 UTC 2017

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 https://hol-theorem-prover.

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

More information about the opentheory-users mailing list