Re: [mizar] Why doesn't this behave like I expect?

[Freek Wiedijk <freek@cs.kun.nl>]

Dear Andrzej (and Piotr),

Thanks for the very quick replies!

>I believe it is an old feature (not ver. 7). After widening
>of the type, we do not round up the result.

I see.  Is there a good reason for this?  Maybe efficiency?

>Because you do not want to correct it, I do not write
>how to fix it.

I already knew how to correct it :-)

My fear was that tomorrow, in class, someone would ask me
"why not just add this one cluster "-> real Element of REAL",
because you just told us that those Nat's are Element of
REAL's!"  And that I then wouldn't have a good reply.

The reason that I'm using "Nat" instead of "natural number"
is that I'm using my two years old tutorial (that now I'm
trying to get up-to-date again.)  So in that one (and in the
PYTHTRIP thing that was derived from it) I used Nat, and I am
a bit afraid to change this, because I don't know how much
trouble that might bring...

By the way, one of my students mailed me, about the exercise
"test the error recovery of Mizar by pasting a random bit
of program text from another programming language in the
middle of a Mizar article":

  Error recovery was good enough to check jordan4 after a
  page of the OCaml manual pasted. The pasted text wasn't in
  the middle of a theorem, but between theorems. Pasting
  random text in the middle of a proof makes mizar *crash*:
  It tries to access memory it shouldn't try to. Strange... I
  thought pascal had no pointers and thus couldn't make that
  kind of errors. Someone should be using OCaml :)

Should I ask him to send that crashing input to someone?  (So
we're currently using 7.0.01.)

Freek