Error Number: 93

Mizar Message:

Missing field of a prefix

Description

While giving a definition to the structure one or more fields of the parent structure are omitted. It does not always means that the field is really missed from definition but it could be invisible for checker or misunderstood by Mizar due to ambiguousness of current environment directives.

Typical examples

Here we are trying to define a new structure ComplexAlgebraStr inherited from structure AlgebraStr which fields use constructors from several articles:

environ
 vocabularies ALGSTR_0, FUNCSDOM, CFUNCDOM, STRUCT_0, BINOP_1, SUBSET_1,
   VECTSP_1, FUNCT_1, ZFMISC_1, PRELAMB, XBOOLE_0;
 notations ALGSTR_0, POLYALG1, BINOP_1, SUBSET_1, FUNCT_2, ZFMISC_1, STRUCT_0;
 constructors ALGSTR_0, POLYALG1;
 registrations ALGSTR_0, POLYALG1;
begin

definition
  let F be doubleLoopStr;
  struct (AlgebraStr over F) ComplexAlgebraStr over F (#
  carrier -> set, addF, multF -> BinOp of the carrier,
  ZeroF, OneF -> Element of the carrier,
  lmult -> Function of [:the carrier of F,the carrier:], the carrier,
  inner_product -> Function of [:the carrier, the carrier:], the carrier of F#);
::>                                                                            *93
end;
::> 93: Missing field of a prefix

The troublemaker in this situation is the 'lmult' symbol. It is recognised by Mizar due to vocabularies VECTSP_1 directive. But actually there is no appropriate notation for it. It means that the notation is supposed to be described in the current article. Then the field 'lmult' is a new one and not inherited from AlgebraStr, therefore, one of the original fields is missing. This happens because the field modes in structures can not be overridden in Mizar language. To get rid of the error message one could add notations VECTSP_1 directive where the notation for original 'lmult' field is contained.

Weird examples

Please contribute