Struct ImportRequest 

pub struct ImportRequest {
    pub audit: bool,
    pub retain: RetainSource,
    pub lean_binder_names: bool,
}

How import_with imports.

Fields

audit: bool

Run the declaration audit (independent recheck of every definition, theorem, opaque and axiom, with its transitive axioms).

retain: RetainSource

lean_binder_names: bool

Carry Lean’s binder names into the kernel terms (arena.local.<depth>.<name>, read back by lean_binder_name). Checking is identical either way; the benchmark protocol keeps them off so its refusal messages stay byte-for-byte what they were.

Trait Implementations

impl Clone for ImportRequest

fn clone(&self) -> ImportRequest

Returns a duplicate of the value.

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

Performs copy-assignment from source.

impl Debug for ImportRequest

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

Formats the value using the given formatter.

impl Default for ImportRequest

fn default() -> ImportRequest

Returns the “default value” for a type.

impl PartialEq for ImportRequest

fn eq(&self, other: &ImportRequest) -> bool

Tests for self and other values to be equal, and is used by ==.

fn ne(&self, other: &Rhs) -> bool

Tests for !=. The default implementation is almost always sufficient, and should not be overridden without very good reason.

impl Eq for ImportRequest

impl StructuralPartialEq for ImportRequest