[mizar] puzzling error *109

[Jesse Alama <alama@stanford.edu>]

I'm trying to redefine the operator * (composition of relations and
functions) for functions having certain specific types.  One example
is the case of an enumeration, which I define as follows:

definition let X be finite set;
  mode enumeration of X -> FinSequence of X means
  len it = card X & rng it = X;
end;

Then I want to say the following, but I get an error:

definition let p be polyhedron,
               f be enumeration of vertices(p),
               P be Permutation of Seg V(p);
  redefine func f*P -> enumeration of vertices(p);
::>              *109
  coherence;
end;

Error 109 is "Invalid order of arguments of redefined constructor".  I
don't see what order I'm getting wrong, since the types of both the
left and right argument of * are the same (namely, Relation).  What
might be going on here?

Thanks,

Jesse

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