Enum Term 

pub enum Term {
    Sort(Universe),
    Var(String),
    Global(String),
    Pi {
        param: String,
        param_type: Box<Term>,
        body_type: Box<Term>,
    },
    Lambda {
        param: String,
        param_type: Box<Term>,
        body: Box<Term>,
    },
    App(Box<Term>, Box<Term>),
    Match {
        discriminant: Box<Term>,
        motive: Box<Term>,
        cases: Vec<Term>,
    },
    Fix {
        name: String,
        body: Box<Term>,
    },
    Lit(Literal),
    Hole,
}

Unified term representation.

Every expression in CoC is a Term:

• Sort(u) - universes (Type 0, Type 1, Prop)
• Var(x) - variables
• Pi - dependent function types: Π(x:A). B
• Lambda - functions: λ(x:A). t
• App - application: f x

Variants

Sort(Universe)

Universe: Type n or Prop

Var(String)

Local variable reference (bound by λ or Π)

Global(String)

Global definition (inductive type or constructor)

Pi

Dependent function type: Π(x:A). B

When B doesn’t mention x, this is just A → B. When B mentions x, this is a dependent type.

Fields

param: String

param_type: Box<Term>

body_type: Box<Term>

Lambda

Lambda abstraction: λ(x:A). t

Fields

param: String

param_type: Box<Term>

body: Box<Term>

App(Box<Term>, Box<Term>)

Application: f x

Match

Pattern matching on inductive types.

match discriminant return motive with cases

• discriminant: the term being matched (must have inductive type)
• motive: λx:I. T — describes the return type
• cases: one case per constructor, in definition order

Fields

discriminant: Box<Term>

motive: Box<Term>

cases: Vec<Term>

Fix

Fixpoint (recursive function).

fix name. body binds name to itself within body. Used for recursive definitions like addition.

Fields

name: String

Name for self-reference within the body

body: Box<Term>

The body of the fixpoint (typically a lambda)

Lit(Literal)

Primitive literal value.

Hardware-native values like i64, f64, String. These compute via CPU ALU, not recursion.

Hole

Hole (implicit argument).

Represents an argument that should be inferred by the type checker. Used in Literate syntax like X equals Y where the type of X/Y is implicit.

Trait Implementations

impl Clone for Term

fn clone(&self) -> Term

Returns a duplicate of the value.

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

Performs copy-assignment from source.

impl Debug for Term

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

Formats the value using the given formatter.

impl Display for Term

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

Formats the value using the given formatter.

impl PartialEq for Term

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

impl StructuralPartialEq for Term