Enum Lean4DoStmt 

pub enum Lean4DoStmt {
    Bind(String, Option<Lean4Type>, Box<Lean4Expr>),
    LetBind(String, Option<Lean4Type>, Box<Lean4Expr>),
    Expr(Box<Lean4Expr>),
    Return(Box<Lean4Expr>),
    Pure(Box<Lean4Expr>),
    If(Box<Lean4Expr>, Vec<Lean4DoStmt>, Vec<Lean4DoStmt>),
}

Statements in a do block.

Variants

Bind(String, Option<Lean4Type>, Box<Lean4Expr>)

let x ← action

LetBind(String, Option<Lean4Type>, Box<Lean4Expr>)

let x := value

Expr(Box<Lean4Expr>)

Plain expression statement: action

Return(Box<Lean4Expr>)

return e

Pure(Box<Lean4Expr>)

pure e

If(Box<Lean4Expr>, Vec<Lean4DoStmt>, Vec<Lean4DoStmt>)

if c then ...

Trait Implementations

impl Clone for Lean4DoStmt

fn clone(&self) -> Lean4DoStmt

Returns a duplicate of the value.

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

Performs copy-assignment from source.

impl Debug for Lean4DoStmt

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

Formats the value using the given formatter.

impl Display for Lean4DoStmt

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

Formats the value using the given formatter.

impl PartialEq for Lean4DoStmt

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