[mizar] a puzzling type error

[Jesse Alama <alama@stanford.edu>]

In my formalization of Poincaré's proof of Euler's polyhedron formula
I need to define various vector spaces.  Currently I'm working on the
simplest vector space; I'm trying to get the MIZAR checker to accept
that it really is a vector space.  As it stands now, I'm having some
trouble with the vector addition operation.  Here's my current
definition:

definition let p be polyhedron, c,d be 0-chain of p;
  func 0-chain-sum(p,c,d) -> 0-chain of p means
  for x being vertex of p,
      y being Element of {0,1}
      holds [x,y] in it
            iff ex u,v being Element of {0,1}
                   st u = c.x &
                      v = d.x &
                      y = u+v;
end;

This definition is accepted in the sense that the only errors are *4's
on the correctness conditions (proofs of which I have temporarily put
aside).  I also have the functor registration

registration let p be polyhedron;
  cluster 0-chain-zero(p) -> 0-chain of p;
end;

for assigning the type 0-chain of p to what will be the zero vector in
the vector space I'm considering.  (Again, I have temporarily put
aside the *4 error on the coherence claim for this cluster.)  Despite
this registration and definition of 0-chain-sum, the statement

for c being 0-chain of p
    holds 0-chain-sum(p,c,0-chain-zero(p)) = c;

is rejected in the sense that the left-hand side of the equation gets
flagged with error *103 ("Unknown functor").  I'm puzzled why this
error has arisen; why might this be going on?

Thanks,

Jesse

PS I'm aware of a workaround, namely existentials:

for c being 0-chain of p, z being 0-chain of p st z = 0-chain-zero(p)
    holds 0-chain-sum(p,c,z) = c;

This statement flagged only with a *4 (naturally), but, if possible,
I'd like to avoid this approach.

-- 
Jesse Alama (alama@stanford.edu)
*104: Unknown structure (http://www.mizar.org)