A trouble with a redefinition

[Piotr Rudnicki <piotr@cs.ualberta.ca>]

Hi:

I have run into a need to add a hidden argument while redefining a functor.

In POLYNOM1 there is the following definition:
 
 definition
  let L be non empty HGrStr,
      a be Element of the carrier of L,
      p be FinSequence of the carrier of L;
  func a ù F -> FinSequence of the carrier of L means
 :: POLYNOM1:def 2  ...

I would like to redefine the above functor for linear combinations
defined as:

definition
  let R be non empty doubleLoopStr,
      A be non empty Subset of the carrier of R;
  mode LinearCombination of A -> FinSequence of the carrier of R means
    ...

My all attempts at the redefinition:

 definition
   let R be associative (non empty doubleLoopStr),
       A be non empty Subset of the carrier of R,
       a be Element of the carrier of R,
       F be Linear_Combination of A;
   redefine func a ù F -> LinearCombination of A means
	. . .

fail because of the hidden argument A.  

Andrzej tells me that in the current implementation the additional
arguments can show up only at the front of the list.  It seems though
that if this restriction is removed life would become a bit easier.

-- 
Piotr Rudnicki