pyk.kore.lexer module

class KoreToken(text, type)[source]

Bases: NamedTuple

text: str: Alias for field number 0

type: TokenType: Alias for field number 1

class TokenType(value)[source]

Bases: Enum

An enumeration.

COLON = 2

COMMA = 1

EOF = 0

ID = 11

KW_ALIAS = 43

KW_AXIOM = 41

KW_CLAIM = 42

KW_ENDMODULE = 35

KW_HOOKED_SORT = 38

KW_HOOKED_SYMBOL = 40

KW_IMPORT = 36

KW_MODULE = 34

KW_SORT = 37

KW_SYMBOL = 39

KW_WHERE = 44

LBRACE = 6

LBRACK = 8

LPAREN = 4

ML_AND = 17

ML_BOTTOM = 15

ML_CEIL = 25

ML_DV = 31

ML_EQUALS = 27

ML_EXISTS = 21

ML_FLOOR = 26

ML_FORALL = 22

ML_IFF = 20

ML_IMPLIES = 19

ML_IN = 28

ML_LEFT_ASSOC = 32

ML_MU = 23

ML_NEXT = 29

ML_NOT = 16

ML_NU = 24

ML_OR = 18

ML_REWRITES = 30

ML_RIGHT_ASSOC = 33

ML_TOP = 14

RBRACE = 7

RBRACK = 9

RPAREN = 5

SET_VAR_ID = 13

STRING = 10

SYMBOL_ID = 12

WALRUS = 3

kore_lexer(it: Iterable[str]) → Iterator[KoreToken][source]