Re: [mizar] the carrier of and [#]

[Jesse Alama <alama@stanford.edu>]

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.

Jesse

-- 
Jesse Alama (alama@stanford.edu)
*950: Too many schemes (http://www.mizar.org)