Enum DeclKind 

pub enum DeclKind {
    Theorem,
    Definition,
    Opaque,
    Axiom,
    Structure,
    Inductive,
    Recursive,
    Instance,
}

The kind of a declaration.

Variants

Theorem

A theorem with a proof body.

Definition

A definition with a definitional body.

Opaque

An opaque definition (body not unfolded during type-checking).

Axiom

An axiom (no body).

Structure

A structure (record type).

Inductive

An inductive type.

Recursive

A recursive definition.

Instance

An instance of a typeclass.

Implementations

impl DeclKind

pub fn has_body(self) -> bool

Returns true if the declaration has a body.

pub fn is_type_decl(self) -> bool

Returns true if this is a type-defining declaration.

pub fn label(self) -> &'static str

Returns a short string label.

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 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

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 Copy for DeclKind

impl Eq for DeclKind

impl StructuralPartialEq for DeclKind