Struct IdrisFunction 

pub struct IdrisFunction {
    pub name: String,
    pub type_sig: IdrisType,
    pub clauses: Vec<(Vec<IdrisPattern>, IdrisExpr)>,
    pub totality: Totality,
    pub visibility: Visibility,
    pub pragmas: Vec<String>,
    pub doc: Option<String>,
}

A top-level Idris 2 function definition.

Fields

name: String

Function name.

type_sig: IdrisType

Type signature (the full type).

clauses: Vec<(Vec<IdrisPattern>, IdrisExpr)>

Function clauses: (patterns, rhs).

totality: Totality

Totality annotation.

visibility: Visibility

Visibility.

pragmas: Vec<String>

Optional %inline or other pragmas.

doc: Option<String>

Optional doc comment.

Implementations

impl IdrisFunction

pub fn new(name: impl Into<String>, ty: IdrisType, body: IdrisExpr) -> Self

Create a new function with a single clause.

pub fn with_clauses( name: impl Into<String>, ty: IdrisType, clauses: Vec<(Vec<IdrisPattern>, IdrisExpr)>, ) -> Self

Create a function with multiple clauses.

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

Emit this function definition.

Trait Implementations

impl Clone for IdrisFunction

fn clone(&self) -> IdrisFunction

Returns a duplicate of the value.

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

Performs copy-assignment from source.

impl Debug for IdrisFunction

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

Formats the value using the given formatter.

impl PartialEq for IdrisFunction

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