<div dir="ltr"><div><div><div><div><div>Hi OpenTheory list,<br><br></div>I am trying to find out more about why an article file I generated causes opentheory to fail. It prints this error:<br><br> FATAL ERROR: opentheory failed:<br> error in file "Test.art" around line 37270:<br> trans<br> 5016<br> def<br> while executing trans command:<br> terms not alpha-equivalent<br><br></div>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?<br><br></div>The failing article can be found (for now) at <a href="https://hol-theorem-prover.org/Test.art" target="_blank">https://hol-theorem-prover.<wbr>org/Test.art</a>.<br><br></div>Cheers,<br></div>Ramana</div>