Enum IdrisExpr 

pub enum IdrisExpr {
    Lit(IdrisLiteral),
    Var(String),
    Qualified(Vec<String>),
    App(Box<IdrisExpr>, Box<IdrisExpr>),
    Lam(Vec<String>, Box<IdrisExpr>),
    Let(String, Box<IdrisExpr>, Box<IdrisExpr>),
    CaseOf(Box<IdrisExpr>, Vec<(IdrisPattern, IdrisExpr)>),
    IfThenElse(Box<IdrisExpr>, Box<IdrisExpr>, Box<IdrisExpr>),
    Do(Vec<IdrisDoStmt>),
    Tuple(Vec<IdrisExpr>),
    ListLit(Vec<IdrisExpr>),
    Annot(Box<IdrisExpr>, Box<IdrisType>),
    Idiom(Box<IdrisExpr>),
    ProofTerm(Box<IdrisExpr>),
    WithPattern(Box<IdrisExpr>, Vec<(IdrisPattern, IdrisExpr)>),
    Infix(String, Box<IdrisExpr>, Box<IdrisExpr>),
    Hole(String),
    Refl,
    AnonHole,
    RecordUpdate(Box<IdrisExpr>, Vec<(String, IdrisExpr)>),
    Neg(Box<IdrisExpr>),
}

An expression in Idris 2.

Variants

Lit(IdrisLiteral)

A literal value.

Var(String)

A variable reference x.

Qualified(Vec<String>)

A fully qualified name Module.name.

App(Box<IdrisExpr>, Box<IdrisExpr>)

Function application f x.

Lam(Vec<String>, Box<IdrisExpr>)

Lambda \x => body.

Let(String, Box<IdrisExpr>, Box<IdrisExpr>)

Let binding let x = val in body.

CaseOf(Box<IdrisExpr>, Vec<(IdrisPattern, IdrisExpr)>)

case scrutinee of { alts }.

IfThenElse(Box<IdrisExpr>, Box<IdrisExpr>, Box<IdrisExpr>)

if cond then t else e.

Do(Vec<IdrisDoStmt>)

A do block: list of statements.

Tuple(Vec<IdrisExpr>)

Tuple (e1, e2, ...).

ListLit(Vec<IdrisExpr>)

List literal [e1, e2, ...].

Annot(Box<IdrisExpr>, Box<IdrisType>)

Type annotation (e : T).

Idiom(Box<IdrisExpr>)

An idiom bracket [| f x y |].

ProofTerm(Box<IdrisExpr>)

A proof term / tactic block believe_me x.

WithPattern(Box<IdrisExpr>, Vec<(IdrisPattern, IdrisExpr)>)

with view pattern expression.

Infix(String, Box<IdrisExpr>, Box<IdrisExpr>)

Infix operator expression a op b.

Hole(String)

A hole ?name.

Refl

refl — reflexivity proof.

AnonHole

?_ — anonymous hole.

RecordUpdate(Box<IdrisExpr>, Vec<(String, IdrisExpr)>)

A record update { field = val }.

Neg(Box<IdrisExpr>)

A negative integer -n.

Trait Implementations

impl Clone for IdrisExpr

fn clone(&self) -> IdrisExpr

Returns a duplicate of the value.

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

Performs copy-assignment from source.

impl Debug for IdrisExpr

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

Formats the value using the given formatter.

impl Display for IdrisExpr

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

Formats the value using the given formatter.

impl PartialEq for IdrisExpr

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