Enum AttributeKind 

pub enum AttributeKind {
    Simp,
    Ext,
    Instance,
    Reducible,
    Irreducible,
    Inline,
    NoInline,
    SpecializeAttr,
    Custom(String),
}

Typed attribute kinds for declarations.

In Lean 4, attributes like @[simp], @[ext], @[reducible] control how the elaborator and tactics treat definitions.

Variants

Simp

@[simp] - add to the simp set

Ext

@[ext] - extensionality lemma

Instance

@[instance] - typeclass instance

Reducible

@[reducible] - mark as reducible for definitional equality

Irreducible

@[irreducible] - mark as irreducible

Inline

@[inline] - inline during compilation

NoInline

@[noinline] - do not inline

SpecializeAttr

@[specialize] - specialization hint

Custom(String)

Custom user attribute

Implementations

impl AttributeKind

pub fn is_custom(&self) -> bool

Check if this is a custom attribute.

pub fn name(&self) -> &str

Get the name of the attribute as a string.

Trait Implementations

impl Clone for AttributeKind

fn clone(&self) -> AttributeKind

Returns a duplicate of the value.

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

Performs copy-assignment from source.

impl Debug for AttributeKind

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

Formats the value using the given formatter.

impl Display for AttributeKind

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

Formats the value using the given formatter.

impl PartialEq for AttributeKind

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

impl StructuralPartialEq for AttributeKind