Menu

#123 Error in Rules testing?

none
open
nobody
None
4
2013-04-25
2013-04-25
Leo Freitas
No

After adding Dialect-aware section management a type error showed up on rewrite1.tex: SimpleHide3 theorem was defined twice. This fix, lead to some tests to fail.

In Eclipse, they were in RewriteTest, whereas in the command line they were at SimpleProverTest. This is weird and confusing. No clue on why. The discrepancy
between expected / achieved result isn't significant either. Something is wrong,
don't know the source.

For now, ignoring the error within Rules....

Discussion


Log in to post a comment.