Error Number: 856

Mizar Message:

Inaccessible requirements directive

Description

A requirements directive needs prerequisite information that is not being supplied by the other environment directives.

For the complete set of requirements, the minimum vocabulary is:

environ
        constructors NUMBERS, XCMPLX_0, XXREAL_0;
        requirements SUBSET, BOOLE, NUMERALS, REAL, ARITHM;

Example

In this example, XXREAL_0 is missing in the constructors directive:

environ

    constructors NUMBERS, XCMPLX_0;     :: missing XXREAL_0
    requirements SUBSET, BOOLE, NUMERALS, REAL, ARITHM;
::>                                          *856

begin

::>
::> 856: Inaccessible requirements directive


WebForm
TopicClassification ErrorMessage
ImplementationDate? N/A
Topic revision: r3 - 2010-08-17 - 17:41:31 - BorisSchminke
 
Mizar TWiki
This site is powered by the TWiki collaboration platformCopyright © by the contributing authors. All material on this collaboration platform is the property of the contributing authors.
Ideas, requests, problems regarding TWiki? Send feedback