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 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).

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_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.