Struct ImportedContext 

pub struct ImportedContext { /* private fields */ }

Owned imported artifacts keep the importer’s stack discipline when released.

Implementations

impl ImportedContext

pub fn retained_source(&self) -> Option<(&str, &Term, &Term)>

The checked type and body of the declaration named by import_audited_retaining_source.

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

The retained checked type and body of name — including an opaque theorem’s proof, which the context itself keeps opaque — when the import was asked to retain it.

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

Every retained declaration with its checked type and body, in export (dependency) order.

Methods from Deref<Target = Context>

pub fn shadows(&self) -> &[(String, String)]

The shadow table, as (written name, identity) pairs, in the order the written names were first shadowed.

pub fn shadow_of(&self, written: &str) -> Option<String>

The identity the written absolute name written denotes, when a shadow redirects it: the table’s own entry, or — for a constant DERIVED from a shadowing declaration (a recursor, an equation lemma, a structure’s constructor or projection) — that constant, whose key spells the identity where the written name spells the name: B2_rec reaches B2✝⟨1⟩_rec exactly when B2 reaches B2✝⟨1⟩.

pub fn shadow_origin(&self, identity: &str) -> Option<&str>

The written name a minted identity was minted for; None for every key no shadow minted.

pub fn shadow_root(&self, key: &str) -> Option<String>

The minted identity key IS, or is DERIVED from (a recursor, an equation lemma, a structure’s constructor or projection, spelled with the identity inside its own key). None for every key no shadow minted or derived from.

pub fn is_live_shadow(&self, identity: &str) -> bool

Whether the minted identity identity is the one its written name denotes NOW — false once a later declaration of that name has been shadowed in over it.

pub fn spelled_by(&self, key: &str) -> Option<String>

The written absolute name that reaches key through a shadow, live or not: the name an identity was minted for, or — for a constant derived from an identity — its key with that name in the identity’s place. None for a key no shadow minted or derived from.

pub fn written_name(&self, key: &str) -> String

How key is WRITTEN here, for output that must read as source. A live identity is written as the name it was minted for; an identity whose name has since been shadowed again is written as that name marked inaccessible (add✝), the way Lean prints an inaccessible name; a constant derived from an identity is written with the identity’s spelling in its place; and a declaration a shadow hides is written with the _root_ escape, which still reaches it. Every other key is written as itself.

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 out_params(&self, name: &str) -> &[usize]

The parameter positions of the class name that are OUTPUTS — Lean’s outParam. An output takes no part in instance MATCHING: the instance determines it, and a mismatch against what the surrounding context expected is an ordinary type error at the use site rather than a different instance. Empty for anything that is not a registered structure.

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

If name is a derived parent-forget edge ({Child}_to{Parent}, generated by Context::add_structure from a flattened field prefix), the parent class it forgets to. Instance resolution uses this to tell a HIERARCHY route apart from an ordinary overlapping instance: two routes to one parent that disagree are an incoherent diamond, where two direct instances are merely overlap.

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 implicit_args(&self, name: &str) -> usize

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

pub fn scope_depth(&self) -> usize

How many scopes are open (0 = the permanent scope).

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

All registered FALLBACK instances, as (type, value) pairs — the lower tier, searched only once Context::instances has been exhausted.

pub fn instance_priority(&self, i: usize) -> i64

The priority of the instance registered at index i (Lean’s default, 1000, for an instance registered before priorities existed or through Context::add_instance).

pub fn instance_search_order(&self) -> Vec<usize>

The order instance resolution must scan Context::instances in — LEAN’S RULE, stated once, here, so no scan site can invent its own:

higher PRIORITY first; among equal priorities, the LATER declaration first.

Earliest-first — what a linear 0..n scan gives — inverts every tie-break a Lean source relies on, silently: both readings type-check and compute different answers.

Returned as indices into instances() so a caller can report WHICH entry won and why.

pub fn instance_search_order_for(&self, goal: &Term) -> (Vec<usize>, usize)

Context::instance_search_order restricted to the candidates that could answer goal — Lean’s getUnify against the discrimination tree (Lean/Meta/SynthInstance.lean:210), in the same order the unrestricted scan would have visited them.

THE INVARIANT, and it is the only one that matters: this is a SUBSET of instance_search_order() containing every entry that could possibly unify, in the same relative order. So it changes what a search PAYS, never what it ANSWERS — and S_spine_extra::the_index_keeps_every_open_candidate_visible_and_the_order_unchanged holds it to both halves.

Returns (candidates, pruned), where pruned is how many entries the index excluded without a unification attempt. Lean’s tree throws that number away; reporting it is what makes “why did this instance not fire?” answerable.

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

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

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

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

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

A global’s per-parameter names and defaults, if recorded.

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

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

This is the record of what was explicitly declared, not the order resolution scans — see Context::instance_search_order for that, and Context::fallback_instances for the lower tier.

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 poly_declaration(&self, name: &str) -> Option<(&[String], &Term)>

A name’s LEVEL TELESCOPE and the type it stands at — for a polymorphic type declaration or a polymorphic definition alike, in that order.

The ordering is the same one Context::get_global uses (a header outranks a body), and it matters for exactly one case: a name re-declared from a definition into an inductive must resolve as the inductive, or typing would read a level telescope the reducer no longer has a body for.

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

Is name a universe-polymorphic TYPE declaration — one with a level telescope and no body?

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 is_derived_aux(&self, name: &str) -> bool

Is name a constant THIS context auto-derived ({I}_rec, {I}_noConfusion, decEq{I}, …) rather than one a human wrote?

The distinction is what lets declaration-time synthesis be idempotent: re-deriving must REPLACE its own prior generation — an inductive is incomplete until its last constructor, so the auxiliaries derived after the first one describe a different type — while never touching a hand-written constant of the same name.

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

The auxiliaries this context derived for a source declaration, in generation order. Inductives own recursors and related products; definitions own equation lemmas.

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.

Three sources, in strict order:

1. the count the declaration stated (Context::add_indexed_inductive) — always wins, so a translator carrying Lean’s own split across is never second-guessed;
2. otherwise the count INFERRED from the registered constructors (see Context::infer_num_params);
3. otherwise the full arity, for a header with no constructors yet — a declaration in progress behaves exactly as it always did.

O(1): the inference is computed once per add_constructor, never per read. This is read on ι-reduction’s argument-skipping path, so a scan here would be a scan inside reduction.

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

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

pub fn auto_auxiliaries(&self) -> bool

Whether eager declaration-time auxiliary synthesis is on.

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

The inductives whose auxiliaries are still OWED — declared, not yet synthesised.

An honest channel rather than silence: a caller can see exactly which declarations would gain constants from a seal. Lean does not tell you, because there synthesis is unconditional and its cost is invisible.

pub fn holds_checked_declaration( &self, name: &str, params: &[String], ty: &Term, body: &Term, transparent_theorem: bool, ) -> bool

Whether name already holds exactly this checked declaration: published through the checked door at the same universe parameters and type, with — for a transparent theorem — the same body, and — for an opaque one, whose body is sealed — the same dependency evidence.

The checked door refuses every existing name, identical or not: it is append-only, as Lean’s environment is. A document read a second time meets its own declarations there, and asks this first, so its second reading registers nothing and refuses nothing.

pub fn holds_assumption(&self, name: &str, params: &[String], ty: &Term) -> bool

Whether name already holds exactly this ASSUMPTION — a bodyless declaration at the same universe parameters and type, published through the assumption door. The door refuses every existing name; this is the question a document read again asks first (see Context::holds_checked_declaration).

pub fn refused_declarations(&self) -> &[(String, String)]

Every declaration the checked gateway REFUSED, as (name, reason), in refusal order.

Empty is the healthy state and the thing to lock: it says every definition in this context was checked or is tracked as owed, and none was silently dropped.

pub fn pending_obligations(&self) -> Vec<(&str, &str)>

Definitions whose body has NOT yet been checked against its declared type, and assumptions whose type has not, each paired with the name it is still waiting for — our #print axioms for deferred obligations.

Pending definitions remain recorded but are unavailable to constant lookup and reduction until their bodies have been checked. Resolving a dependency retries its waiting definitions and exposes only those whose checks succeed.

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 iter_universe_polys( &self, ) -> impl Iterator<Item = (&str, &[String], &Term, &Term)>

Iterate over the universe-polymorphic definitions: name, level parameters, type, body.

pub fn unit_constructor(&self, inductive: &str) -> Option<&str>

A non-indexed, fieldless singleton at any universe. Recursive and indexed single-constructor families do not have the unit eta rule.

pub fn k_constructor(&self, inductive: &str) -> Option<&str>

The unique constructor of a K-like proposition: no stored fields beyond the uniform parameters. Its indices still need conversion at each use.

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

pub fn reducibility(&self, name: &str) -> Reducibility

name’s declared reducibility (the default when nothing was declared).

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

Whether name is @[irreducible] — THE PREDICATE Transparency::Excluding wants.

One lookup in one map, so a reducer may ask it once per δ-candidate without the question costing more than the unfolding would have.

pub fn simp_rules(&self) -> &[SimpRule]

Every registered rewrite rule, in registration order.

pub fn simp_rules_for(&self, head: &str) -> impl Iterator<Item = &SimpRule>

The rules whose left-hand side has head symbol head — THE DISPATCH DOOR.

A rewriter walking a term asks this once per subterm and gets only the rules that can possibly match it. Never scan Context::simp_rules linearly from a hot path.

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

Whether name is registered as a @[simp] lemma.

Trait Implementations

impl Deref for ImportedContext

type Target = Context

The resulting type after dereferencing.

fn deref(&self) -> &Context

Dereferences the value.

impl Drop for ImportedContext

fn drop(&mut self)

Executes the destructor for this type.