Enum DeclKind 

pub enum DeclKind {
    Definition,
    Theorem,
    Axiom,
    Inductive,
    Structure,
    Class,
    Instance,
    Namespace,
    Section,
    Import,
    Variable,
    Open,
    Attribute,
    HashCmd,
    Mutual,
    Derive,
    Notation,
    Universe,
    Other,
}

A coarse kind tag for a top-level declaration, used as part of DeclFingerprint equality. Two decls with the same name but different kinds are treated as unrelated (Delete + Insert rather than Modified).

Variants

Definition

def / noncomputable def

Theorem

theorem / lemma

Axiom

axiom

Inductive

inductive

Structure

structure

Class

class

Instance

instance

Namespace

namespace … end

Section

section … end

Import

import

Variable

variable

Open

open

Attribute

attribute

HashCmd

#check, #eval, #print, …

Mutual

mutual { … }

Derive

deriving

Notation

notation / infixl / infixr / …

Universe

universe

Other

Any other / anonymous declaration

Implementations

impl DeclKind

pub fn of(decl: &Decl) -> Self

Derive the DeclKind from a Decl value.

Trait Implementations

impl Clone for DeclKind

fn clone(&self) -> DeclKind

Returns a duplicate of the value.

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

Performs copy-assignment from source.

impl Debug for DeclKind

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

Formats the value using the given formatter.

impl Eq for DeclKind

impl Hash for DeclKind

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 DeclKind

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

Equality operator ==.

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

Inequality operator !=.

impl StructuralPartialEq for DeclKind