[Logiweb] Diagnose error

[Klaus Ebbe Grue]

On Sat, 25 Jun 2005, Kasper H0st Frederiksen wrote:

> We all remember the warning that, if you write a proof line that uses
> a double successor operation you have to remenber to write (b')' not b''.
>
> Now, if line L1 uses the correct form: (b')', and you want to use L1 in 
> another line L2(f.eks for a modus ponens), AND you make a mistake while 
> typing L2 then pyk shoule provede a diagnose page with a 'Lemma/Proof 
> mismatch -error', but it does not. The diagnose dvi file is corrupted but the 
> body file is fine. Latex says this is because of a double superscript error.
>
> I am not 100% shure this is the correct interpretation of the problem, but I 
> have uptoaded a page that ilustrates the error
> http://www.diku.dk/~grue/logiweb/20050502/home/tofu/diagnose-error/fixed/

Thanks for pointing this out.

Looking up
   http://www.diku.dk/~grue/logiweb/20050502/home/tofu/diagnose-error/
   fixed/diagnose/tex/page.log
states that the error is in line 123. Line 121-123 in
   http://www.diku.dk/~grue/logiweb/20050502/home/tofu/diagnose-error/
   fixed/diagnose/tex/page.tex
looks like this:
   ...\hskip0em plus2.0em
   '
   '\linebreak [0]...
The problem is that diagnoses are produced after macro expansion, so the 
parenthesis has disappeared before the diagnose is generated.
   The only long term solution (which I forgot when writing the new Peano 
page) is to render the successor-function not as
   #1.'
but as
   #1.{}'
(with a newline after #1.). That will render a double successor as {}'{}' 
which is legal TeX.

Klaus