Enum Token 

pub enum Token {
    Ident(String),
    Nat(String),
    Literal(String),
    Underscore,
    NamedHole(String),
    Theorem,
    Lemma,
    Axiom,
    Forall,
    Exists,
    Fun,
    Colon,
    Assign,
    Comma,
    Dot,
    Arrow,
    MapsTo,
    Pipe,
    Turnstile,
    LParen,
    RParen,
    LBrace,
    RBrace,
    LBracket,
    RBracket,
    LStrict,
    RStrict,
    Op(String),
    Eof,
}

Variants

Ident(String)

Nat(String)

Literal(String)

String or character literal, including quotes.

Underscore

_

NamedHole(String)

?name

Theorem

Keywords / symbols

Lemma

Axiom

Forall

Exists

Fun

Colon

:

Assign

:=

Comma

,

Dot

.

Arrow

→ or ->

MapsTo

=> or ↦

Pipe

| (pattern / match; also conclusion search prefix before -)

Turnstile

|- conclusion-search marker (produced by lexer when seeing | -)

LParen

RParen

LBrace

RBrace

LBracket

RBracket

LStrict

⦃

RStrict

⦄

Op(String)

Binary / unary operators and other symbol tokens

Eof

End of input

Implementations

impl Token

pub fn is_ident_like(&self) -> bool

Trait Implementations

impl Clone for Token

fn clone(&self) -> Token

Returns a duplicate of the value.

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

Performs copy-assignment from source.

impl Debug for Token

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

Formats the value using the given formatter.

impl Display for Token

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

Formats the value using the given formatter.

impl Eq for Token

impl PartialEq for Token

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

Equality operator ==.

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

Inequality operator !=.

impl StructuralPartialEq for Token