Enum IdrisAttribute 

pub enum IdrisAttribute {
    Auto,
    Interface,
    Search,
    Totality(Totality),
    Inline,
    Static,
}

Elaboration attributes that can be applied to types, functions, or constructors.

Variants

Auto

@{auto} — auto-implicit solve.

Interface

@{interface} — interface auto-search.

Search

@{search} — proof search.

Totality(Totality)

[totality] — totality requirement.

Inline

[inline] — inline hint.

Static

[static] — static argument.

Trait Implementations

impl Clone for IdrisAttribute

fn clone(&self) -> IdrisAttribute

Returns a duplicate of the value.

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

Performs copy-assignment from source.

impl Debug for IdrisAttribute

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

Formats the value using the given formatter.

impl Display for IdrisAttribute

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

Formats the value using the given formatter.

impl PartialEq for IdrisAttribute

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

impl StructuralPartialEq for IdrisAttribute