-
Notifications
You must be signed in to change notification settings - Fork 81
/
TokensScript.sml
35 lines (31 loc) · 1.11 KB
/
TokensScript.sml
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
(* generated by Lem from semantics/tokens.lem *)
open bossLib Theory Parse res_quanTheory
open finite_mapTheory listTheory pairTheory pred_setTheory integerTheory
open set_relationTheory sortingTheory stringTheory wordsTheory
val _ = new_theory "Tokens"
val _ = Hol_datatype `
token =
WhitespaceT of num
| NewlineT
| HashT | LparT | RparT | StarT | CommaT | ArrowT | DotsT | ColonT | SealT
| SemicolonT | EqualsT | DarrowT | LbrackT | RbrackT | UnderbarT | LbraceT
| BarT | RbraceT | AbstypeT | AndT | AndalsoT | AsT | CaseT | DatatypeT | DoT
| ElseT | EndT | EqtypeT | ExceptionT | FnT | FunT | FunctorT | HandleT | IfT
| InT | IncludeT | InfixT | InfixrT | LetT | LocalT | NonfixT | OfT | OpT
| OpenT | OrelseT | RaiseT | RecT | SharingT | SigT | SignatureT | StructT
| StructureT | ThenT | TypeT | ValT | WhereT | WhileT | WithT | WithtypeT
| ZeroT
| DigitT of string
| NumericT of string
| IntT of int
| HexintT of string
| WordT of string
| HexwordT of string
| RealT of string
| StringT of string
| CharT of string
| TyvarT of string
| AlphaT of string
| SymbolT of string
| LongidT of string`;
val _ = export_theory()