Enum RetainSource 

pub enum RetainSource {
    Nothing,
    Named(HashSet<String>),
    EveryProof,
}

Which checked declarations an import copies out, type and body, beyond what the context keeps. A theorem’s or opaque’s proof is opaque in the context; only retention keeps it.

Variants

Nothing

Nothing is copied.

Named(HashSet<String>)

The named declarations (importer keys) that have a body.

EveryProof

Every checked theorem and opaque declaration of the export.

Trait Implementations

impl Clone for RetainSource

fn clone(&self) -> RetainSource

Returns a duplicate of the value.

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

Performs copy-assignment from source.

impl Debug for RetainSource

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

Formats the value using the given formatter.

impl Default for RetainSource

fn default() -> RetainSource

Returns the “default value” for a type.

impl PartialEq for RetainSource

fn eq(&self, other: &RetainSource) -> 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 RetainSource

impl StructuralPartialEq for RetainSource