Enum TokenKind 

pub enum TokenKind {
    Module,
    Use,
    Const,
    Var,
    Type,
    Init,
    Action,
    Invariant,
    Property,
    Fairness,
    Func,
    And,
    Or,
    Not,
    Implies,
    Iff,
    All,
    Any,
    Choose,
    In,
    For,
    If,
    Then,
    Else,
    Let,
    With,
    Require,
    Changes,
    Always,
    Eventually,
    LeadsTo,
    Enabled,
    WeakFair,
    StrongFair,
    True,
    False,
    Nat,
    Int,
    Bool,
    String_,
    Set,
    Seq,
    Dict,
    Option_,
    Some_,
    None_,
    LParen,
    RParen,
    LBrace,
    RBrace,
    LBracket,
    RBracket,
    Comma,
    Colon,
    Semicolon,
    Dot,
    DotDot,
    Arrow,
    FatArrow,
    Prime,
    Pipe,
    Eq,
    Ne,
    Lt,
    Le,
    Gt,
    Ge,
    Plus,
    Minus,
    Star,
    Slash,
    Percent,
    Union,
    Intersect,
    Diff,
    SubsetOf,
    PlusPlus,
    Head,
    Tail,
    Len,
    Keys,
    Values,
    Powerset,
    UnionAll,
    Ampersand,
    Assign,
    Integer(i64),
    StringLit(String),
    Ident(String),
    Comment(String),
    DocComment(String),
    Eof,
    Error(String),
}

The kind of token.

Variants

Module

module

Use

use

Const

const

Var

var

Type

type

Init

init

Action

action

Invariant

invariant

Property

property

Fairness

fairness

Func

func - user-defined helper function

And

and

Or

or

Not

not

Implies

implies

Iff

iff

All

all (universal quantifier, Python-like)

Any

any (existential quantifier, Python-like)

Choose

choose (deterministic selection)

In

in

For

for

If

if

Then

then

Else

else

Let

let

With

with

Require

require

Changes

changes

Always

always

Eventually

eventually

LeadsTo

leads_to

Enabled

enabled

WeakFair

weak_fair

StrongFair

strong_fair

True

true

False

false

Nat

Nat

Int

Int

Bool

Bool

String_

String

Set

Set

Seq

Seq

Dict

dict - Python-like dictionary type (lowercase only)

Option_

Option

Some_

Some

None_

None

LParen

(

RParen

)

LBrace

{

RBrace

}

LBracket

[

RBracket

]

Comma

,

Colon

:

Semicolon

;

Dot

.

DotDot

..

Arrow

->

FatArrow

=>

Prime

' (prime for next-state variables)

Pipe

|

Eq

==

Ne

!=

Lt

<

Le

<=

Gt

>

Ge

>=

Plus

+

Minus

-

Star

*

Slash

/

Percent

%

Union

union

Intersect

intersect

Diff

diff

SubsetOf

subset_of

PlusPlus

++

Head

head - get first element of sequence

Tail

tail - get all but first element of sequence

Len

len - get length of sequence/set/function

Keys

keys - get domain of function as set

Values

values - get range of function as set

Powerset

powerset - get set of all subsets

UnionAll

union_all - distributed union (union of all sets in set)

Ampersand

&

Assign

=

Integer(i64)

Integer literal

StringLit(String)

String literal (without quotes)

Ident(String)

Identifier

Comment(String)

Single-line comment // ...

DocComment(String)

Documentation comment /// ...

Eof

End of file

Error(String)

Lexer error

Implementations

impl TokenKind

pub fn is_keyword(&self) -> bool

Check if this token is a keyword.

pub fn keyword(ident: &str) -> Option<TokenKind>

Get the keyword for a given identifier, if any.

pub fn is_trivia(&self) -> bool

Check if this is a trivia token (comment, whitespace).

Trait Implementations

impl Clone for TokenKind

fn clone(&self) -> TokenKind

Returns a duplicate of the value.

fn clone_from(&mut self, source: &Self)

Performs copy-assignment from source.

impl Debug for TokenKind

fn fmt(&self, f: &mut Formatter<'_>) -> Result

Formats the value using the given formatter.

impl Display for TokenKind

fn fmt(&self, f: &mut Formatter<'_>) -> Result

Formats the value using the given formatter.

impl PartialEq for TokenKind

fn eq(&self, other: &TokenKind) -> bool

Tests for self and other values to be equal, and is used by ==.

fn ne(&self, other: &Rhs) -> bool

Tests for !=. The default implementation is almost always sufficient, and should not be overridden without very good reason.

impl StructuralPartialEq for TokenKind