Module expr 

The kernel core’s expression store: a maximally shared DAG with de Bruijn indices.

Every structurally distinct expression is one ExprId. Construction goes through Store::intern, so building the same node twice yields the same id and structural equality is an integer compare. Each node carries its loose-bound-variable range and whether it contains free variables or universe parameters, computed once at construction; substitution skips any subterm those flags prove it cannot touch.

Binder names and binder annotations are not part of a node: they are irrelevant to typing and conversion, and dropping them lets fun (x : A) => x and fun (y : A) => y share one id.

Nodes created while a declaration is checked live in a separate scratch region, marked by the top bit of their id. When the declaration is done, Store::end_scratch drops them in O(1), so transient terms never accumulate across a hundred thousand declarations — while a result computed purely from persistent terms (a definition’s body at given universe levels) can still be interned persistently mid-declaration (Store::with_persistent) and cached for every later declaration.

Structs

ExprId

LitId

NatId

Store

StrId

Enums

Lit

A LOGOS literal with no Lean counterpart. Nat and Text literals are Node::NatLit and Node::StrLit. An integer is canonical: one that fits i64 is Int, any other BigInt. A float is held by its bits, so equal literals are one id and 0.0/-0.0 stay apart.

Node

Type Aliases

Args

The arguments of an application spine; most spines fit inline.