[Date Prev][Date Next]
[Chronological]
[Thread]
[Top]
Re: [mizar] the carrier of and [#]
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...
Best,
Adam Naumowicz
======================================================================
Department of Applied Logic fax. +48 (85) 745-7662
Institute of Computer Science tel. +48 (85) 745-7559 (office)
University of Bialystok e-mail: adamn@mizar.org
Sosnowa 64, 15-887 Bialystok, Poland http://math.uwb.edu.pl/~adamn/
======================================================================