Struct CaptureRequest 

pub struct CaptureRequest<'a> {
    pub context: &'a Context,
    pub base: EnvironmentBase,
    pub conversion: ConversionDiscipline,
    pub target: &'a str,
    pub opaque_proofs: &'a BTreeMap<String, Term>,
}

Fields

context: &'a Context

base: EnvironmentBase

conversion: ConversionDiscipline

target: &'a str

opaque_proofs: &'a BTreeMap<String, Term>

The checked proofs of the opaque theorems in the target’s closure (the target’s own included, when it is one). A checked context publishes only an opaque theorem’s header.