Enum IdrisDecl 

pub enum IdrisDecl {
    Func(IdrisFunction),
    Data(IdrisData),
    Record(IdrisRecord),
    Interface(IdrisInterface),
    Implementation(IdrisImpl),
    Namespace(String, Vec<IdrisDecl>),
    Mutual(Vec<IdrisDecl>),
    Parameters(Vec<(String, IdrisType)>, Vec<IdrisDecl>),
    Pragma(String),
    Postulate(String, IdrisType, Visibility),
    Comment(String),
    Blank,
}

A top-level declaration in an Idris 2 module.

Variants

Func(IdrisFunction)

A function definition.

Data(IdrisData)

A data declaration.

Record(IdrisRecord)

A record declaration.

Interface(IdrisInterface)

An interface declaration.

Implementation(IdrisImpl)

An implementation block.

Namespace(String, Vec<IdrisDecl>)

A namespace N where block.

Mutual(Vec<IdrisDecl>)

A mutual block for mutually recursive definitions.

Parameters(Vec<(String, IdrisType)>, Vec<IdrisDecl>)

A parameters block: parameters (x : T) where.

Pragma(String)

A % pragma: %name T x, y, z.

Postulate(String, IdrisType, Visibility)

A type-level postulate (axiom).

Comment(String)

A line comment.

Blank

A blank separator.

Implementations

impl IdrisDecl

pub fn emit(&self, indent: usize) -> String

Emit this declaration at the given indent level.

Trait Implementations

impl Clone for IdrisDecl

fn clone(&self) -> IdrisDecl

Returns a duplicate of the value.

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

Performs copy-assignment from source.

impl Debug for IdrisDecl

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

Formats the value using the given formatter.

impl PartialEq for IdrisDecl

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