Suggestion: Use expandable mode definition of Field

In VECTSP_1, I find the reservation block:

 reserve F for Field,
         x for Element of F,
         V for VectSp-like add-associative right_zeroed right_complementable
           (non empty VectSpStr over F),
         v for Element of V;

Just above this block the definition of Field is given:

definition let F be add-associative right_zeroed right_complementable Abelian
   associative left_unital distributive (non empty doubleLoopStr);
 mode VectSp of F is VectSp-like
  add-associative right_zeroed right_complementable Abelian
   (non empty VectSpStr over F);
end;

The reservation block would thus be simplified if V were declared to have type VectSp? of F. It would also benefit those who search the MML for vector spaces.

Article name:	VECTSP_1
MML version:	4.76.959

|

Follow up

Never mind -- I see now that Abelian is part of the definition of VectSp? of F, but the reservation block does not include that attribute. -- JesseAlama - 24 Jan 2007