Re: [mizar] a puzzling type error

[Adam Naumowicz <adamn@math.uwb.edu.pl>]

Hi Jesse,

On Fri, 26 Jan 2007, Jesse Alama wrote:

> I also have the functor registration
>
> registration let p be polyhedron;
>  cluster 0-chain-zero(p) -> 0-chain of p;
> end;

What you've been trying to use is a quite new feature of registrations 
which should allow for registering clusters of attributes (empty list of 
attributes in this case next to '0-chain of p') that are applicable only 
to terms having a type which is more specific than the original type of 
the term's constructor (as a result of a redefinition). At the moment it 
seems that the semantics of this feature hasn't been fully decided on yet, 
and the functionality seems, so to speak, a bit under-implemented. But 
whatever semantics is going to 'win' eventually, it's rather unlikely that 
it would mean registering not only the attributes as it does now, but also 
"registering the type" in the way redefinitions work now.

So in your case, you should redefine the '0-chain-zero(p)' functor to have 
a needed type, or even better, use the required result type ('0-chain of 
p') directly in the definition of '0-chain-zero(p)' if this is possible.

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/
======================================================================