Enum CoqElementType 

pub enum CoqElementType {
    Whitespace,
    Newline,
    Comment,
    StringLiteral,
    NumberLiteral,
    Identifier,
    Theorem,
    Lemma,
    Remark,
    Fact,
    Corollary,
    Proposition,
    Definition,
    Example,
    Fixpoint,
    CoFixpoint,
    Inductive,
    CoInductive,
    Record,
    Structure,
    Variant,
    Module,
    Section,
    End,
    Require,
    Import,
    Export,
    Proof,
    Qed,
    Defined,
    Admitted,
    If,
    Then,
    Else,
    Type,
    Prop,
    Set,
    Check,
    Print,
    Search,
    Locate,
    About,
    Match,
    With,
    Forall,
    Exists,
    Fun,
    Let,
    In,
    Class,
    Instance,
    Intros,
    Simpl,
    Reflexivity,
    Rewrite,
    Apply,
    Exact,
    Assumption,
    Auto,
    Trivial,
    Discriminate,
    Injection,
    Inversion,
    Destruct,
    Induction,
    Generalize,
    Clear,
    Unfold,
    Fold,
    Compute,
    Eval,
    Show,
    Goal,
    Goals,
    Undo,
    Restart,
    Admit,
    Abort,
    Parameter,
    Axiom,
    Variable,
    Hypothesis,
    Chapter,
    Open,
    Close,
    Scope,
    Notation,
    Infix,
    Reserved,
    Bind,
    Delimit,
    Arguments,
    Implicit,
    Coercion,
    Identity,
    Canonical,
    Arrow,
    DoubleArrow,
    Colon,
    Semicolon,
    Comma,
    Dot,
    Pipe,
    Underscore,
    Equal,
    Plus,
    Minus,
    Star,
    Slash,
    Percent,
    Less,
    Greater,
    LessEqual,
    GreaterEqual,
    NotEqual,
    Tilde,
    At,
    Question,
    Exclamation,
    Ampersand,
    Hash,
    Dollar,
    Backslash,
    Caret,
    LeftParen,
    RightParen,
    LeftBracket,
    RightBracket,
    LeftBrace,
    RightBrace,
    DoubleColon,
    DoubleColonEqual,
    ColonEqual,
    Turnstile,
    And,
    Or,
    LeftArrow,
    Root,
    Declaration,
    Statement,
    Expression,
    Error,
    Eof,
}

Element types for the Coq AST.

Variants

Whitespace

Whitespace.

Newline

Newline.

Comment

Comment.

StringLiteral

String literal.

NumberLiteral

Number literal.

Identifier

Identifier.

Theorem

Theorem keyword.

Lemma

Lemma keyword.

Remark

Remark keyword.

Fact

Fact keyword.

Corollary

Corollary keyword.

Proposition

Proposition keyword.

Definition

Definition keyword.

Example

Example keyword.

Fixpoint

Fixpoint keyword.

CoFixpoint

CoFixpoint keyword.

Inductive

Inductive keyword.

CoInductive

CoInductive keyword.

Record

Record keyword.

Structure

Structure keyword.

Variant

Variant keyword.

Module

Module keyword.

Section

Section keyword.

End

End keyword.

Require

Require keyword.

Import

Import keyword.

Export

Export keyword.

Proof

Proof keyword.

Qed

Qed keyword.

Defined

Defined keyword.

Admitted

Admitted keyword.

If

If keyword.

Then

Then keyword.

Else

Else keyword.

Type

Type keyword.

Prop

Prop keyword.

Set

Set keyword.

Check

Check keyword.

Print

Print keyword.

Search

Search keyword.

Locate

Locate keyword.

About

About keyword.

Match

Match keyword.

With

With keyword.

Forall

Forall symbol or keyword.

Exists

Exists symbol or keyword.

Fun

Fun keyword.

Let

Let keyword.

In

In keyword.

Class

Class keyword.

Instance

Instance keyword.

Intros

Intros tactic keyword.

Simpl

Simpl tactic keyword.

Reflexivity

Reflexivity tactic keyword.

Rewrite

Rewrite tactic keyword.

Apply

Apply tactic keyword.

Exact

Exact tactic keyword.

Assumption

Assumption tactic keyword.

Auto

Auto tactic keyword.

Trivial

Trivial tactic keyword.

Discriminate

Discriminate tactic keyword.

Injection

Injection tactic keyword.

Inversion

Inversion tactic keyword.

Destruct

Destruct tactic keyword.

Induction

Induction tactic keyword.

Generalize

Generalize tactic keyword.

Clear

Clear tactic keyword.

Unfold

Unfold tactic keyword.

Fold

Fold tactic keyword.

Compute

Compute tactic keyword.

Eval

Eval tactic keyword.

Show

Show tactic keyword.

Goal

Goal keyword.

Goals

Goals keyword.

Undo

Undo command keyword.

Restart

Restart command keyword.

Admit

Admit tactic keyword.

Abort

Abort command keyword.

Parameter

Parameter keyword.

Axiom

Axiom keyword.

Variable

Variable keyword.

Hypothesis

Hypothesis keyword.

Chapter

Chapter keyword.

Open

Open keyword.

Close

Close keyword.

Scope

Scope keyword.

Notation

Notation keyword.

Infix

Infix keyword.

Reserved

Reserved keyword.

Bind

Bind keyword.

Delimit

Delimit keyword.

Arguments

Arguments keyword.

Implicit

Implicit keyword.

Coercion

Coercion keyword.

Identity

Identity keyword.

Canonical

Canonical keyword.

Arrow

Arrow ->.

DoubleArrow

Double arrow =>.

Colon

Colon :.

Semicolon

Semicolon ;.

Comma

Comma ,.

Dot

Dot ..

Pipe

Pipe |.

Underscore

Underscore _.

Equal

Equal =.

Plus

Plus +.

Minus

Minus -.

Star

Star *.

Slash

Slash /.

Percent

Percent %.

Less

Less than <.

Greater

Greater than >.

LessEqual

Less than or equal to <=.

GreaterEqual

Greater than or equal to >=.

NotEqual

Not equal <>.

Tilde

Tilde ~.

At

At @.

Question

Question mark ?.

Exclamation

Exclamation mark !.

Ampersand

Ampersand &.

Hash

Hash #.

Dollar

Dollar $.

Backslash

Backslash \.

Caret

Caret ^.

LeftParen

Left parenthesis (.

RightParen

Right parenthesis ).

LeftBracket

Left bracket [.

RightBracket

Right bracket ].

LeftBrace

Left brace {.

RightBrace

Right brace }.

DoubleColon

Double colon ::.

DoubleColonEqual

Double colon equal ::=.

ColonEqual

Colon equal :=.

Turnstile

Turnstile |-.

And

Logical AND /\.

Or

Logical OR \/.

LeftArrow

Left arrow <-.

Root

Root node.

Declaration

Declaration node.

Statement

Statement node.

Expression

Expression node.

Error

Parsing error.

Eof

End of stream.

Trait Implementations

impl Clone for CoqElementType

fn clone(&self) -> CoqElementType

Returns a duplicate of the value.

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

Performs copy-assignment from source.

impl Debug for CoqElementType

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

Formats the value using the given formatter.

impl<'de> Deserialize<'de> for CoqElementType

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

where __D: Deserializer<'de>,

Deserialize this value from the given Serde deserializer.

impl ElementType for CoqElementType

type Role = UniversalElementRole

The associated role type for this element kind.

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

Returns the general syntactic role of this element.

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

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

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

Returns true if this element matches the specified universal role.

fn is_root(&self) -> bool

Returns true if this element represents the root of the parsed tree.

fn is_error(&self) -> bool

Returns true if this element represents an error condition.

impl From<CoqTokenType> for CoqElementType

fn from(token: CoqTokenType) -> Self

Converts to this type from the input type.

impl Hash for CoqElementType

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 CoqElementType

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

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

where __S: Serializer,

Serialize this value into the given Serde serializer.

impl Copy for CoqElementType

impl Eq for CoqElementType

impl StructuralPartialEq for CoqElementType