Tokens fall in six classes, and the end token eof closes the array.

• Reserved words, the 24 words int, bool, void, if, else, while, for, return, true, false, auto, delete, new, nullptr, this, class, public, private, virtual, override, namespace, template, typename and operator.

• Type identifiers, TypeId, with an uppercase initial.

• Variable identifiers, VarId, with a lowercase initial or _, naming variables, fields, functions and methods.

• Namespace identifiers, NsId, the identifiers of either case that :: follows.

• Decimal integer literals, IntLit.

• Operators and punctuation, with [=] as a single token by the longest match rule.

There is no token >>, so Stack<Stack<int>> closes with two tokens >.

\begin{array}{lcl} \textit{Token} & ::= & \textit{Keyword}\ \mid\ \textit{TypeId}\ \mid\ \textit{VarId}\ \mid\ \textit{NsId}\ \mid\ \textit{IntLit}\ \mid\ \textit{Symbol} \\ \textit{Keyword} & ::= & \texttt{int}\ \mid\ \texttt{bool}\ \mid\ \texttt{void}\ \mid\ \texttt{class} \\ & \mid & \texttt{public}\ \mid\ \texttt{private}\ \mid\ \texttt{new}\ \mid\ \texttt{delete} \\ & \mid & \texttt{nullptr}\ \mid\ \texttt{this}\ \mid\ \texttt{virtual} \\ & \mid & \texttt{override}\ \mid\ \texttt{namespace}\ \mid\ \texttt{template} \\ & \mid & \texttt{typename}\ \mid\ \texttt{auto}\ \mid\ \texttt{if}\ \mid\ \texttt{else}\ \mid\ \texttt{while}\ \mid\ \texttt{for}\ \mid\ \texttt{return} \\ & \mid & \texttt{true}\ \mid\ \texttt{false}\ \mid\ \texttt{operator} \\ \textit{TypeId} & ::= & \textit{Upper}\ \textit{IdentChar}^{*} \\ \textit{VarId} & ::= & \big(\ \textit{Lower}\ \mid\ \texttt{\_}\ \big)\ \textit{IdentChar}^{*} \\ \textit{NsId} & ::= & \textit{TypeId}\ \mid\ \textit{VarId} \\ \textit{IntLit} & ::= & \textit{Digit}\ \textit{Digit}^{*} \\ \textit{Symbol} & ::= & \texttt{[=]} \\ & \mid & \texttt{==}\ \mid\ \texttt{!=}\ \mid\ \texttt{<=}\ \mid\ \texttt{>=}\ \mid\ \texttt{\&\&}\ \mid\ \texttt{||}\ \mid\ \texttt{->}\ \mid\ \texttt{::}\ \mid\ \texttt{--}\ \mid\ \texttt{++} \\ & \mid & \texttt{+}\ \mid\ \texttt{-}\ \mid\ \texttt{*}\ \mid\ \texttt{/}\ \mid\ \texttt{\%}\ \mid\ \texttt{<}\ \mid\ \texttt{>}\ \mid\ \texttt{!}\ \mid\ \texttt{?}\ \mid\ \texttt{:}\ \mid\ \texttt{=} \\ & \mid & \texttt{(}\ \mid\ \texttt{)}\ \mid\ \texttt{\{}\ \mid\ \texttt{\}}\ \mid\ \texttt{[}\ \mid\ \texttt{]}\ \mid\ \texttt{,}\ \mid\ \texttt{;}\ \mid\ \texttt{.}\ \mid\ \texttt{\&}\ \mid\ \texttt{\textasciitilde} \\ \textit{IdentChar} & ::= & \textit{Upper}\ \mid\ \textit{Lower}\ \mid\ \textit{Digit}\ \mid\ \texttt{\_} \\ \textit{Upper} & ::= & \texttt{A}\ \mid\ \ldots\ \mid\ \texttt{Z} \\ \textit{Lower} & ::= & \texttt{a}\ \mid\ \ldots\ \mid\ \texttt{z} \\ \textit{Digit} & ::= & \texttt{0}\ \mid\ \ldots\ \mid\ \texttt{9} \\ \textit{Skip} & ::= & \textit{WhiteSpace}\ \mid\ \texttt{//}\ \textit{NotNewline}^{*}\ \textit{Newline}^{?} \end{array}

The lexer covers the input by a sequence of Token and Skip, discards Skip, and takes the longest match at each position. A line comment ends at a newline or at the end of the input. The symbols of three characters are tried before those of two and of one.

An identifier is classified by its initial after the reserved words are excluded. A further pass over the token array marks as an NsId every identifier whose next token is ::, of either case.

The pass qualifiers runs after the automaton, so it sees neither white space nor comments and marks std :: vector as it marks std::vector. The parser runs the automaton on each line of the Preproc output alone and the pass once on the tokens of all the lines, so a :: that starts a line marks the identifier that ends the line before.

That class is what lets a qualified name open a type where the case convention alone would read a variable, so std::vector<int> needs no reserved word.

The function lex maps a string to an array of tokens ended by eof. It runs the automaton Lexer.run and then the pass of Definition 1.1.2. It discards white space and line comments, reads the longest run of digits as an integer literal, the longest run of identifier characters as an identifier, and tries the symbols of three, two and one characters in that order. Any other character is a lexical error.

The lexer also rejects what C++ would read otherwise, so that every Core C++ program is a C++ program with the same meaning.

• It rejects a keyword of C++ or an alternative representation such as and outside the reserved words of the subset (N4659 §5.11, Tables 5 and 6).

• It rejects an integer literal with a leading 0, which C++ reads in octal, and one above 2147483647, to which C++ gives a type wider than int.

• It reads -- and ++ as tokens that no production uses, so 5--2 fails as in C++, where the longest match gives --.

The automaton Lexer.run is partial, so Lean records an opaque constant that carries the type and not the body, and no property of it is proved here.