Enum ErasedDecl 

pub enum ErasedDecl {
    Def {
        name: String,
        body: ErasedExprExt,
    },
    Axiom {
        name: String,
    },
    Inductive {
        name: String,
        ctor_count: u32,
    },
}

An erased module declaration.

Variants

Def

A function definition.

Fields

name: String

body: ErasedExprExt

Axiom

An axiom (no body).

Fields

name: String

Inductive

An inductive type with constructor count.

Fields

name: String

ctor_count: u32

Implementations

impl ErasedDecl

pub fn name(&self) -> &str

Return the name of this declaration.

pub fn is_def(&self) -> bool

Return true if this is a function definition.

Trait Implementations

impl Clone for ErasedDecl

fn clone(&self) -> ErasedDecl

Returns a duplicate of the value.

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

Performs copy-assignment from source.

impl Debug for ErasedDecl

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

Formats the value using the given formatter.