Enum Term 

pub enum Term {
    Sort(Universe),
    Var(String),
    Global(String),
    Const {
        name: String,
        levels: Vec<Universe>,
    },
    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>,
    },
    MutualFix {
        defs: Vec<(String, Term)>,
        index: usize,
    },
    Let {
        name: String,
        ty: Box<Term>,
        value: Box<Term>,
        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)

Const

A universe-polymorphic global referenced at explicit levels — name.{ℓ₀, ℓ₁, …}. Global is the monomorphic case (no level arguments); Const instantiates a stored universe-polymorphic definition’s universe parameters with levels.

Fields

name: String

levels: Vec<Universe>

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)

MutualFix

MUTUAL fixpoint — a block of mutually-recursive functions (K3).

mutualfix { f₀ := b₀, …, fₙ := bₙ }.index binds ALL of f₀ … fₙ within EVERY body bᵢ (that is the mutual part), and the whole term reduces to the index-th definition. It is the body of a mutual inductive block’s recursor: Even.rec’s fixpoint calls Odd.rec’s on the smaller sub-proof and vice versa. Each body’s type is inferred structurally from its λ-telescope (like the single Fix); termination is the MUTUAL Giménez guard — a call to ANY member must pass a structurally-smaller argument at that member’s recursive position.

Fields

defs: Vec<(String, Term)>

The mutually-recursive definitions, (name, body), in block order. Every name is in scope in every body.

index: usize

Which definition this occurrence denotes (and reduces to).

Let

Local definition: let name : ty := value in body.

name is bound to value (of type ty) transparently within body — so the body is type-checked and reduced with name ≡ value (ZETA), not as an opaque hypothesis. The surface let; the sharing seam for the elaborator.

Fields

name: String

ty: Box<Term>

value: Box<Term>

body: Box<Term>

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