Theory Tokens

chapter ‹Generated by Lem from ‹semantics/tokens.lem›.›

theory "Tokens" 

imports
  Main
  "HOL-Library.Datatype_Records"
  "LEM.Lem_pervasives_extra"

begin 

― ‹‹open import Pervasives_extra››
― ‹‹ Tokens for Standard ML.  NB, not all of them are used in CakeML ››
datatype token =
  WhitespaceT " nat " | NewlineT | LexErrorT
| HashT | LparT | RparT | StarT | CommaT | ArrowT | DotsT | ColonT | SealT
| SemicolonT | EqualsT | DarrowT | LbrackT | RbrackT | UnderbarT | LbraceT
| BarT | RbraceT | AndT | AndalsoT | AsT | CaseT | DatatypeT
| ElseT | EndT | EqtypeT | ExceptionT | FnT | FunT | HandleT | IfT
| InT | IncludeT | LetT | LocalT | OfT | OpT
| OpenT | OrelseT | RaiseT | RecT | RefT | SharingT | SigT | SignatureT | StructT
| StructureT | ThenT | TypeT | ValT | WhereT | WhileT | WithT | WithtypeT
| IntT " int "
| HexintT " string "
| WordT " nat "
| RealT " string "
| StringT " string "
| CharT " char "
| TyvarT " string "
| AlphaT " string "
| SymbolT " string "
| LongidT " string " " string "
| FFIT " string "
end