[Date Prev][Date Next]
[Chronological]
[Thread]
[Top]
Re: [mizar] A question on "registrations"
On Mon, 5 Apr 2010, Ozyavas, Adem wrote:
Line 6711 has a functor defintion whose argument type is FinSequence-yielding FinSequence.
I am getting the error *136 (non registered cluster). I believe the existence of that type should be proved.
I checked the PRE_POLY.miz and there is the existence cluster:
registration
cluster FinSequence-yielding Function;
end;
I included the PRE_POLY to "registrations" directive but this time I am getting the error *103 (unknown functor) at line 6718
where 'fs' is the FinSequence-yielding FinSequence.
Apart from PRE_POLY, you also need the registration which states that f.j
is Function-like, i.e. FUNCOP_1.
Best,
Adam Naumowicz
=======================================================================
Dept. of Programming and Formal Methods Fax: +48(85)7457662
Institute of Informatics Tel: +48(85)7457559 (office)
University of Bialystok E-mail: adamn@mizar.org
Sosnowa 64, 15-887 Bialystok, Poland http://math.uwb.edu.pl/~adamn/
=======================================================================