Struct Context 

pub struct Context { /* private fields */ }

Typing context: maps variable names to their types.

The context is immutable-by-default: extend creates a new context with the additional binding, preserving the original.

Also stores global definitions:

• Inductive types (e.g., Nat : Type 0)
• Constructors (e.g., Zero : Nat, Succ : Nat -> Nat)
• Declarations (e.g., hypotheses like h1 : P -> Q)

Implementations

impl Context

pub fn new() -> Self

Create an empty context.

pub fn register_struct_info(&mut self, name: &str, info: StructInfo)

Record structure metadata (used by Context::add_structure).

pub fn struct_info(&self, name: &str) -> Option<&StructInfo>

The structure metadata for an inductive type name, if it is a registered structure (record). None for ordinary inductives — eta never fires for them.

pub fn struct_of_constructor(&self, ctor: &str) -> Option<(&str, &StructInfo)>

If ctor is the constructor of a registered structure, return (structure name, its info). Used to detect an η-expandable constructor head.

pub fn set_implicit_args(&mut self, name: &str, count: usize)

Record that the global name has count leading implicit parameters, so the surface elaborator inserts that many inferred arguments at each application.

pub fn implicit_args(&self, name: &str) -> usize

How many leading parameters of name are implicit (0 if none/unknown).

pub fn add_instance(&mut self, ty: Term, value: Term)

Register a typeclass instance: a value of type ty (e.g. mk Nat Zero of type Inhabited Nat). The elaborator resolves an instance-implicit argument by searching these for a ty that unifies with the required class type.

pub fn add_coercion(&mut self, from: Term, to: Term, coe: Term)

Register a coercion coe : from → to — the elaborator may insert it when an argument of type from appears where to is expected.

pub fn coercions(&self) -> &[(Term, Term, Term)]

All registered coercions, as (from, to, coe) triples.

pub fn set_binder_kinds(&mut self, name: &str, kinds: Vec<ParamKind>)

Record a global’s per-parameter kinds (implicit/explicit/instance, in order), so the elaborator can insert implicit and instance arguments at their real positions.

pub fn binder_kinds(&self, name: &str) -> Option<&[ParamKind]>

A global’s per-parameter kinds, if recorded.

pub fn instances(&self) -> &[(Term, Term)]

All registered typeclass instances, as (type, value) pairs.

pub fn add_universe_poly( &mut self, name: &str, params: Vec<String>, ty: Term, body: Term, )

Register a universe-polymorphic definition name.{params} : ty := body. A Term::Const { name, levels } reference later instantiates params with levels (the .{ℓ…} syntax), so one definition is reused at every level.

pub fn get_universe_poly( &self, name: &str, ) -> Option<&(Vec<String>, Term, Term)>

Look up a universe-polymorphic definition: (universe params, type, body).

pub fn add(&mut self, name: &str, ty: Term)

Add a local binding to this context (mutates in place).

pub fn get(&self, name: &str) -> Option<&Term>

Look up a local variable’s type in the context.

pub fn extend(&self, name: &str, ty: Term) -> Context

Create a new context extended with an additional local binding.

Does not mutate the original context.

pub fn add_inductive(&mut self, name: &str, sort: Term)

Register an inductive type.

The sort is the type of the inductive (e.g., Type 0 for Nat).

All of the arity is treated as uniform parameters (0 indices) unless set_inductive_params records a smaller parameter count — see add_indexed_inductive.

pub fn add_structure( &mut self, name: &str, params: &[(&str, Term)], fields: &[(&str, Term)], )

Register a STRUCTURE (record) {name} (params) := {name}_mk (fields) — a one-constructor inductive with auto-derived projections and definitional eta.

params are the leading type parameters (A : Type 0), (B : Type 0), …; fields are (fst : A), (snd : B), … where a field type may reference the params and any EARLIER field (by name). Registers:

• the inductive {name} : Π(params). Type 0,
• the constructor {name}_mk : Π(params). Π(fields). {name} params,
• a projection {name}_{fieldᵢ} : Π(params). Π(s:{name} params). Tᵢ for each field (its body a match on s), and
• the StructInfo that gates the eta rule.

The structure lives in Type 0 (fields over Type 0 carriers) — the common case for the algebraic hierarchy.

pub fn add_indexed_inductive( &mut self, name: &str, sort: Term, num_params: usize, )

Register an INDEXED inductive: sort is its full arity Π(params). Π(indices). Sort, of which the first num_params leading arguments are uniform parameters and the rest are indices that vary per constructor (e.g. Eq with num_params == 2).

pub fn set_inductive_params(&mut self, name: &str, num_params: usize)

Record how many leading arguments of name’s arity are uniform parameters.

pub fn inductive_arity(&self, name: &str) -> usize

The full arity of an inductive — the number of leading Πs in its sort (Nat → 0, TList : Type → Type → 1, Eq : Type → A → A → Prop → 3). 0 for an unknown name.

pub fn inductive_declared_params(&self, name: &str) -> Option<usize>

The EXPLICITLY declared parameter count for name, or None if the inductive was registered without one. Reduction uses this to skip exactly the parameters of an indexed constructor (refl A x → 2), falling back to a syntactic heuristic for the legacy inductives that never declared a split — so their ι-reduction is untouched.

pub fn inductive_num_params(&self, name: &str) -> usize

How many leading arguments of name’s arity are uniform PARAMETERS. Defaults to the full arity (so a non-indexed inductive is all parameters, 0 indices).

pub fn inductive_num_indices(&self, name: &str) -> usize

How many trailing arguments of name’s arity are INDICES (arity − parameters).

pub fn add_constructor(&mut self, name: &str, inductive: &str, ty: Term)

Register a constructor for an inductive type.

The ty is the full type of the constructor (e.g., Nat for Zero, Nat -> Nat for Succ).

Constructors are tracked in registration order for match expressions.

pub fn add_declaration(&mut self, name: &str, ty: Term)

Add a declaration (typed assumption/hypothesis).

Used for proof certification where hypotheses are assumed. Example: h1 : P -> Q

pub fn add_definition(&mut self, name: String, ty: Term, body: Term)

Register a definition: name : type := body

Definitions are transparent and unfold during normalization (delta reduction). This distinguishes them from declarations (axioms) which have no body.

pub fn get_global(&self, name: &str) -> Option<&Term>

Look up a global definition (inductive, constructor, definition, or declaration).

Returns the type of the global.

pub fn is_definition(&self, name: &str) -> bool

Check if a name is a definition (has a body that can be unfolded).

pub fn get_definition_body(&self, name: &str) -> Option<&Term>

Get the body of a definition, if it exists.

Returns None for axioms, constructors, and inductives (only definitions have bodies).

pub fn get_definition_type(&self, name: &str) -> Option<&Term>

Get the type of a definition, if it exists.

pub fn is_constructor(&self, name: &str) -> bool

Check if a name is a constructor.

pub fn constructor_inductive(&self, name: &str) -> Option<&str>

Get the inductive type a constructor belongs to.

pub fn is_inductive(&self, name: &str) -> bool

Check if a name is an inductive type.

pub fn get_constructors(&self, inductive: &str) -> Vec<(&str, &Term)>

Get all constructors for an inductive type, in registration order.

Returns a vector of (constructor_name, constructor_type) pairs.

pub fn iter_declarations(&self) -> impl Iterator<Item = (&str, &Term)>

Iterate over all declarations (hypotheses).

Used by the certifier to find hypothesis by type.

pub fn iter_definitions(&self) -> impl Iterator<Item = (&str, &Term, &Term)>

Iterate over all definitions.

Used by the UI to display definitions.

pub fn iter_inductives(&self) -> impl Iterator<Item = (&str, &Term)>

Iterate over all inductive types.

Used by the UI to display inductive types.

pub fn add_constructor_checked( &mut self, name: &str, inductive: &str, ty: Term, ) -> KernelResult<()>

Add a constructor with strict positivity checking.

Returns an error if the inductive type appears negatively in the constructor type. This prevents paradoxes like:

Inductive Bad := Cons : (Bad -> False) -> Bad

pub fn add_mutual_inductives( &mut self, block: &[MutualInductive], ) -> KernelResult<()>

Register a MUTUAL block of inductives whose constructors may reference one another (Even/Odd, Tree/Forest). Strict positivity is checked over the WHOLE block up front — a sibling occurrence is a recursive occurrence, a sibling in a negative position is a cross-block paradox and rejected — and the registration is TRANSACTIONAL: if any constructor violates positivity, nothing is added. On success every member’s header (with its parameter split), every constructor, and the block-membership registry are populated, ready for the auto-derived mutual recursors.

pub fn mutual_block_of(&self, name: &str) -> Option<&[String]>

The mutual block name belongs to (the full ordered member list), or None if name is a standalone inductive. Used by the recursor derivation to give every block member a motive and route sibling recursion.

pub fn add_nested_inductive( &mut self, decl: &NestedDecl, ) -> KernelResult<NestedInfo>

Register a NESTED inductive (RTree := rnode : TList RTree → RTree) by compiling it — via the UNTRUSTED inductive_compile front-end — to a mutual block plus conversion isos, then registering the block and CHECKING every iso through the trusted kernel. A mis-compiled sibling is caught by mutual positivity; a mis-typed iso is caught here (its inferred type must match its declared conversion type). Soundness rests entirely on those trusted checks — the compiler adds no trusted code, exactly as Lean lowers nested inductives to mutual.

pub fn add_hint(&mut self, name: &str)

Register a theorem as a hint for the auto tactic.

Hints are theorems that auto will try to apply when decision procedures fail. This allows auto to “learn” from proven theorems.

pub fn get_hints(&self) -> &[String]

Get all registered hints.

Returns the names of theorems registered as hints.

pub fn is_hint(&self, name: &str) -> bool

Check if a theorem is registered as a hint.

Trait Implementations

impl Clone for Context

fn clone(&self) -> Context

Returns a duplicate of the value.

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

Performs copy-assignment from source.

impl Debug for Context

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

Formats the value using the given formatter.

impl Default for Context

fn default() -> Context

Returns the “default value” for a type.