TWiki> Mizar Web>ErrorNo856 (2010-08-17, BorisSchminke)EditAttach

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
Edit | Attach | Print version | History: r3 < r2 < r1 | Backlinks | Raw View | Raw edit | More topic actions
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