Enum Node 

pub enum Node {
    BVar(u32),
    FVar(u32),
    Sort(LevelId),
    Const(NameId, LevelsId),
    App(ExprId, ExprId),
    Lam(ExprId, ExprId),
    Pi(ExprId, ExprId),
    Let(ExprId, ExprId, ExprId),
    NatLit(NatId),
    StrLit(StrId),
    Proj(NameId, u32, ExprId),
    Match(ExprId, ExprId, ExprId),
    Fix(ExprId),
    MutualFix(ExprId, u32),
    Seq(ExprId, ExprId),
    Nil,
    Lit(LitId),
}

Variants

BVar(u32)

FVar(u32)

Sort(LevelId)

Const(NameId, LevelsId)

App(ExprId, ExprId)

Lam(ExprId, ExprId)

Pi(ExprId, ExprId)

Let(ExprId, ExprId, ExprId)

NatLit(NatId)

StrLit(StrId)

Proj(NameId, u32, ExprId)

Match(ExprId, ExprId, ExprId)

LOGOS: match disc return motive with cases, the cases a Node::Seq chain in constructor order.

Fix(ExprId)

LOGOS: fix f => body, with f bound as BVar 0 in body.

MutualFix(ExprId, u32)

LOGOS: the index-th member of a mutual fixpoint block whose members (a Node::Seq chain) are each bound in every body, the first member outermost.

Seq(ExprId, ExprId)

A non-empty list of expressions: its first element and the rest (Node::Nil at the end). Only Node::Match and Node::MutualFix hold one.

Nil

Lit(LitId)

A LOGOS literal with no Lean counterpart.

Trait Implementations

impl Clone for Node

fn clone(&self) -> Node

Returns a duplicate of the value.

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

Performs copy-assignment from source.

impl Debug for Node

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

Formats the value using the given formatter.

impl Hash for Node

fn hash<__H: Hasher>(&self, state: &mut __H)

Feeds this value into the given Hasher.

fn hash_slice<H>(data: &[Self], state: &mut H)

where H: Hasher, Self: Sized,

Feeds a slice of this type into the given Hasher.

impl PartialEq for Node

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

impl Eq for Node

impl StructuralPartialEq for Node