Error Number: 203

Mizar Message:

Unknown token, maybe the forbidden underscore character used in an identifier

Description

This error is generated under two conditions: * You are using an underscore where one is not allowed * An unknown token is detected

This can be confusing because underscores are allowed in many circumstances, but this error can lead you to believe the problem is an underscore when it is not.

-- GregFrascadore - 2009-07-20

Typical examples

Based on a proof from PARTFUN3. The problem here is not use of an underscore, but of a missing underscore.

environ

 vocabularies PARTFUN1, RELAT_1, FINSEQ_4, FUNCT_1, BOOLE, FUNCOP_1, PARTFUN2,
      COMPLEX1;
 notations TARSKI, XBOOLE_0, SUBSET_1, RELAT_1, FUNCT_1, RELSET_1, PARTFUN1,
      FUNCT_2, FUNCOP_1;
 constructors PARTFUN1, FUNCOP_1;
 registrations XBOOLE_0, RELAT_1, FUNCT_1;
 requirements SUBSET, BOOLE;


begin

reserve x,X for set;
reserve C,D for non empty set;
reserve c for Element of C;
reserve d for Element of D;
reserve f for PartFunc of C,D;

definition
  let C,D;
  let f,X;
  canceled 2;
  pred f is_constant_on X means :Def3:
     ex d st for c st c in X /\ dom f holds f/.c = d;
end;

theorem Th58:
  X /\ dom f = {} implies f is_constant on X
::>                           *203
proof
  assume A1: X /\ dom f = {};
  now consider d being Element of D;
    take d;
    let c;
    thus c in X /\ dom f implies f/.c = d by A1;
  end;
  hence thesis by Def3;
end;

::>
::> 203: Unknown token, maybe the forbidden underscore character used in an identifier