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]¶