Enum LeanTokenType 

pub enum LeanTokenType {
    Root,
    Eof,
    Axiom,
    Constant,
    Def,
    Example,
    Inductive,
    Lemma,
    Namespace,
    Open,
    Private,
    Protected,
    Section,
    Structure,
    Theorem,
    Universe,
    Variable,
    Variables,
    End,
    Import,
    Export,
    Prelude,
    Noncomputable,
    Partial,
    Unsafe,
    Mutual,
    Where,
    Have,
    Show,
    Suffices,
    Let,
    In,
    If,
    Then,
    Else,
    Match,
    With,
    Fun,
    Do,
    For,
    While,
    Break,
    Continue,
    Return,
    Try,
    Catch,
    Finally,
    Throw,
    Identifier,
    IntegerLiteral,
    FloatLiteral,
    StringLiteral,
    CharLiteral,
    Plus,
    Minus,
    Star,
    Slash,
    Percent,
    Caret,
    Hash,
    Ampersand,
    Pipe,
    Tilde,
    Bang,
    Question,
    At,
    Dollar,
    Arrow,
    FatArrow,
    Eq,
    Ne,
    Lt,
    Le,
    Gt,
    Ge,
    And,
    Or,
    Not,
    Append,
    Cons,
    LeftParen,
    RightParen,
    LeftBrace,
    RightBrace,
    LeftBracket,
    RightBracket,
    LeftAngle,
    RightAngle,
    Semicolon,
    Colon,
    Comma,
    Dot,
    DotDot,
    ColonEq,
    ColonColon,
    Whitespace,
    Newline,
    Comment,
    Error,
    SourceFile,
    Function,
    ParameterList,
    Parameter,
    BlockExpression,
    LetStatement,
    ExpressionStatement,
    IdentifierExpression,
    LiteralExpression,
    BooleanLiteral,
    ParenthesizedExpression,
    BinaryExpression,
    UnaryExpression,
    CallExpression,
    FieldExpression,
    IndexExpression,
    IfExpression,
    MatchExpression,
    LoopExpression,
    WhileExpression,
    ForExpression,
    BreakExpression,
    ContinueExpression,
    ReturnExpression,
    StructExpression,
    TupleExpression,
    ArrayExpression,
    RangeExpression,
    ClosureExpression,
    AsyncBlockExpression,
    UnsafeBlockExpression,
    TryExpression,
    AwaitExpression,
    MacroCall,
    Path,
    PathSegment,
    GenericArgs,
    TypePath,
    TupleType,
    ArrayType,
    SliceType,
    ReferenceType,
    PointerType,
    FunctionType,
    TraitObjectType,
    ImplTraitType,
    InferredType,
    NeverType,
    Pattern,
    IdentifierPattern,
    WildcardPattern,
    TuplePattern,
    StructPattern,
    TupleStructPattern,
    SlicePattern,
    ReferencePattern,
    LiteralPattern,
    RangePattern,
    OrPattern,
    RestPattern,
    StructDeclaration,
    EnumDeclaration,
    UnionDeclaration,
    TraitDeclaration,
    ImplDeclaration,
    ModuleDeclaration,
    UseDeclaration,
    ConstDeclaration,
    StaticDeclaration,
    TypeAliasDeclaration,
    ExternBlock,
    ExternFunction,
    Attribute,
    Visibility,
    GenericParams,
    GenericParam,
    TypeParam,
    ConstParam,
    LifetimeParam,
    WhereClause,
    WherePredicate,
    ReturnType,
    FieldList,
    Field,
    Variant,
    VariantList,
    AssociatedItem,
    TraitItem,
    ImplItem,
}

Token types for the Lean language.

Variants

Root

Root node.

Eof

End of stream.

Axiom

axiom keyword.

Constant

constant keyword.

Def

def keyword.

Example

example keyword.

Inductive

inductive keyword.

Lemma

lemma keyword.

Namespace

namespace keyword.

Open

open keyword.

Private

private keyword.

Protected

protected keyword.

Section

section keyword.

Structure

structure keyword.

Theorem

theorem keyword.

Universe

universe keyword.

Variable

variable keyword.

Variables

variables keyword.

End

end keyword.

Import

import keyword.

Export

export keyword.

Prelude

prelude keyword.

Noncomputable

noncomputable keyword.

Partial

partial keyword.

Unsafe

unsafe keyword.

Mutual

mutual keyword.

Where

where keyword.

Have

have keyword.

Show

show keyword.

Suffices

suffices keyword.

Let

let keyword.

In

in keyword.

If

if keyword.

Then

then keyword.

Else

else keyword.

Match

match keyword.

With

with keyword.

Fun

fun keyword.

Do

do keyword.

For

for keyword.

While

while keyword.

Break

break keyword.

Continue

continue keyword.

Return

return keyword.

Try

try keyword.

Catch

catch keyword.

Finally

finally keyword.

Throw

throw keyword.

Identifier

Identifier.

IntegerLiteral

Integer literal.

FloatLiteral

Floating point literal.

StringLiteral

String literal.

CharLiteral

Character literal.

Plus

Plus operator +.

Minus

Minus operator -.

Star

Multiplication operator *.

Slash

Division operator /.

Percent

Modulo operator %.

Caret

Exponentiation operator ^.

Hash

Hash sign #.

Ampersand

Bitwise AND operator &.

Pipe

Bitwise OR operator |.

Tilde

Bitwise NOT operator ~.

Bang

Logical NOT operator !.

Question

Question mark ?.

At

At sign @.

Dollar

Dollar sign $.

Arrow

Arrow ->.

FatArrow

Fat arrow =>.

Eq

Equality operator =.

Ne

Inequality operator !=.

Lt

Less than operator <.

Le

Less than or equal operator <=.

Gt

Greater than operator >.

Ge

Greater than or equal operator >=.

And

Logical AND operator &&.

Or

Logical OR operator ||.

Not

not operator.

Append

Append operator ++.

Cons

Cons operator ::.

LeftParen

Left parenthesis (.

RightParen

Right parenthesis ).

LeftBrace

Left brace {.

RightBrace

Right brace }.

LeftBracket

Left bracket [.

RightBracket

Right bracket ].

LeftAngle

Left angle bracket ⟨.

RightAngle

Right angle bracket ⟩.

Semicolon

Semicolon ;.

Colon

Colon :.

Comma

Comma ,.

Dot

Dot ..

DotDot

Double dot ...

ColonEq

Assignment operator :=.

ColonColon

Double colon ::.

Whitespace

Whitespace.

Newline

Newline.

Comment

Comment.

Error

Error token.

SourceFile

Source file.

Function

Function declaration.

ParameterList

Parameter list.

Parameter

Parameter.

BlockExpression

Block expression.

LetStatement

Let statement.

ExpressionStatement

Expression statement.

IdentifierExpression

Identifier expression.

LiteralExpression

Literal expression.

BooleanLiteral

Boolean literal.

ParenthesizedExpression

Parenthesized expression.

BinaryExpression

Binary expression.

UnaryExpression

Unary expression.

CallExpression

Call expression.

FieldExpression

Field access expression.

IndexExpression

Index access expression.

IfExpression

If expression.

MatchExpression

Match expression.

LoopExpression

Loop expression.

WhileExpression

While loop expression.

ForExpression

For loop expression.

BreakExpression

Break expression.

ContinueExpression

Continue expression.

ReturnExpression

Return expression.

StructExpression

Struct literal expression.

TupleExpression

Tuple literal expression.

ArrayExpression

Array literal expression.

RangeExpression

Range expression.

ClosureExpression

Closure expression.

AsyncBlockExpression

Async block expression.

UnsafeBlockExpression

Unsafe block expression.

TryExpression

Try expression.

AwaitExpression

Await expression.

MacroCall

Macro call.

Path

Path.

PathSegment

Path segment.

GenericArgs

Generic arguments.

TypePath

Type path.

TupleType

Tuple type.

ArrayType

Array type.

SliceType

Slice type.

ReferenceType

Reference type.

PointerType

Pointer type.

FunctionType

Function type.

TraitObjectType

Trait object type.

ImplTraitType

Impl trait type.

InferredType

Inferred type _.

NeverType

Never type !.

Pattern

Pattern.

IdentifierPattern

Identifier pattern.

WildcardPattern

Wildcard pattern _.

TuplePattern

Tuple pattern.

StructPattern

Struct pattern.

TupleStructPattern

Tuple struct pattern.

SlicePattern

Slice pattern.

ReferencePattern

Reference pattern.

LiteralPattern

Literal pattern.

RangePattern

Range pattern.

OrPattern

Or pattern.

RestPattern

Rest pattern ...

StructDeclaration

Struct declaration.

EnumDeclaration

Enum declaration.

UnionDeclaration

Union declaration.

TraitDeclaration

Trait declaration.

ImplDeclaration

Impl block declaration.

ModuleDeclaration

Module declaration.

UseDeclaration

Use declaration.

ConstDeclaration

Const declaration.

StaticDeclaration

Static declaration.

TypeAliasDeclaration

Type alias declaration.

ExternBlock

Extern block.

ExternFunction

Extern function.

Attribute

Attribute.

Visibility

Visibility modifier.

GenericParams

Generic parameters.

GenericParam

Generic parameter.

TypeParam

Type parameter.

ConstParam

Const parameter.

LifetimeParam

Lifetime parameter.

WhereClause

Where clause.

WherePredicate

Where predicate.

ReturnType

Return type specification.

FieldList

Field list.

Field

Field declaration.

Variant

Enum variant.

VariantList

Variant list.

AssociatedItem

Associated item.

TraitItem

Trait item.

ImplItem

Impl item.

Trait Implementations

impl Clone for LeanTokenType

fn clone(&self) -> LeanTokenType

Returns a duplicate of the value.

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

Performs copy-assignment from source.

impl Debug for LeanTokenType

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

Formats the value using the given formatter.

impl<'de> Deserialize<'de> for LeanTokenType

fn deserialize<__D>(__deserializer: __D) -> Result<Self, __D::Error>

where __D: Deserializer<'de>,

Deserialize this value from the given Serde deserializer.

impl From<LeanTokenType> for LeanElementType

fn from(token: LeanTokenType) -> Self

Converts to this type from the input type.

impl Hash for LeanTokenType

fn hash<__H: Hasher>(&self, state: &mut __H)

Feeds this value into the given Hasher.

fn hash_slice<H>(data: &[Self], state: &mut H)

where H: Hasher, Self: Sized,

Feeds a slice of this type into the given Hasher.

impl PartialEq for LeanTokenType

fn eq(&self, other: &LeanTokenType) -> 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 Serialize for LeanTokenType

fn serialize<__S>(&self, __serializer: __S) -> Result<__S::Ok, __S::Error>

where __S: Serializer,

Serialize this value into the given Serde serializer.

impl TokenType for LeanTokenType

const END_OF_STREAM: Self = Self::Error

A constant representing the end of the input stream.

type Role = UniversalTokenRole

The associated role type for this token kind.

fn is_ignored(&self) -> bool

Returns true if this token represents trivia (whitespace, comments, etc.).

fn role(&self) -> Self::Role

Returns the general syntactic role of this token.

fn is_role(&self, role: Self::Role) -> bool

Returns true if this token matches the specified language-specific role.

fn is_universal(&self, role: UniversalTokenRole) -> bool

Returns true if this token matches the specified universal role.

fn is_comment(&self) -> bool

Returns true if this token represents a comment.

fn is_whitespace(&self) -> bool

Returns true if this token represents whitespace.

fn is_error(&self) -> bool

Returns true if this token represents an error condition.

fn is_end_of_stream(&self) -> bool

Returns true if this token represents the end of the input stream.

impl Copy for LeanTokenType

impl Eq for LeanTokenType

impl StructuralPartialEq for LeanTokenType