Error Number: 138

Mizar Message:

Cannot identify a local constant, free in the default type

Description

The locus being declared depends upon a hidden variable which is also a locus and must also be declared.

-- GregFrascadore - 2009-07-18

Typical example

Here C depends upon hidden S, which must also be declared.

environ
    vocabularies AMI_1,BOOLE,SETFAM_1;
    registrations XBOOLE_0;
    requirements BOOLE;
    notations NAT_1,NUMBERS,SETFAM_1,SUBSET_1,TARSKI,XBOOLE_0;
    constructors NAT_1,NUMBERS,SETFAM_1,SUBSET_1,TARSKI,XBOOLE_0;

begin

    reserve S for Subset of NAT;
    reserve C for Cover of S;

    definition
        let C;
::>         *138
        attr C is with_non-empty_elements means
            not {} in C;
    end;

::> 138: Cannot identify a local constant, free in the default type

The problem can be fixed by declaring S.

    definition
        let S, C;
        ...
    end;