Type Alias LeanToken 

pub type LeanToken = Token<LeanTokenType>;

A token produced by the Lean lexer, combining a token type with its source location.

Aliased Type

pub struct LeanToken {
    pub kind: LeanTokenType,
    pub span: Range<usize>,
}

Fields

kind: LeanTokenType

The kind/category of this kind (e.g., keyword, identifier, number)

span: Range<usize>

The byte range in the source text that this kind occupies