Struct RebuiltEnvironment 

pub struct RebuiltEnvironment {
    pub context: Context,
    pub target: String,
    pub target_level_params: Vec<String>,
    pub target_type: Term,
    pub target_proof: Term,
    pub target_is_theorem: bool,
    pub target_is_opaque: bool,
    pub independent: Vec<(String, IndependentVerdict)>,
    pub axioms: AxiomUsage,
    pub assumptions: Vec<(String, Vec<String>, Term)>,
    pub proofs: BTreeMap<String, Term>,
    pub depth: usize,
}

A rebuilt environment: the checked context and what the checks found.

Fields

context: Context

The context, rebuilt from the base with every entry kernel-checked.

target: String

target_level_params: Vec<String>

The target’s universe parameters, type and proof.

target_type: Term

target_proof: Term

target_is_theorem: bool

Whether the target is a theorem whose proof may unfold during conversion.

target_is_opaque: bool

Whether the target is a checked opaque value or proof whose body stays sealed.

independent: Vec<(String, IndependentVerdict)>

Every checked declaration term under the second kernel, by declaration name.

axioms: AxiomUsage

The transitive assumptions of the target’s statement AND proof — #print axioms.

assumptions: Vec<(String, Vec<String>, Term)>

Each assumption the environment declares, with its universe parameters and type.

proofs: BTreeMap<String, Term>

The checked proofs of the environment’s opaque theorems — evidence the context does not publish, kept for re-emission.

depth: usize

The maximum term depth in the certificate, which sized the stack the rebuild needs.

Implementations

impl RebuiltEnvironment

pub fn independently_agreed(&self) -> bool

true when every checked term was corroborated by the independent kernel.