Adam Naumowicz <adamn@math.uwb.edu.pl> writes:
On Wed, 4 Apr 2007, Jesse Alama wrote:
Sorry, I didn't give this enough thought - the error *103 is reported
by the analyzer, the second pass of the verifier which checks the
syntactic ant type correctness - it knows nothing of the equality of
[#]G' and 'the carrier of G' - they are made equal only in the
equalizer. So you can't use '[#]G' where the type correctness of '(#)'
requires an argument of the type 'Finsequence of the carrier of G'.
OK, I understand now why I got the error. Would it be possible to
incorporate the equalizer into the analyzer, so that statements like
the ones I made would be acceptable?
Theoretically, it would be possible to implement some of actions now
done in the equalizer (part of the checker) to be performed in the
analyzer, but I'm affraid that'd mean a thorough redesign of the whole
checker's architecture...
I thought you'd say that. One could say that the problem I faced is
due to my inexperience with the system, which is true, but MIZAR would
be a better system if statements such as mine weren't rejected. What
I wrote is malformed, and I understand why that's so, but it is
intuitively well-formed and thus an ideal MIZAR system would accept
it.