[opentheory-users] Debugging a failing trans

Joe Leslie-Hurd joe at leslie-hurd.com
Thu Apr 27 19:43:24 UTC 2017

Hi Ramana,

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:
>  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
> _______________________________________________
> opentheory-users mailing list
> opentheory-users at gilith.com
> http://www.gilith.com/opentheory/mailing-list

More information about the opentheory-users mailing list