Re: A question on "registrations"
Adam Naumowicz <[email protected]>
| Newsgroups | gmane.comp.mathematics.mizar |
|---|---|
| Message-ID | <Pine.GSO.4.61.1004051730580.29104@math> |
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: [email protected] Sosnowa 64, 15-887 Bialystok, Poland http://math.uwb.edu.pl/~adamn/ =======================================================================