Enum InstanceTier 

pub enum InstanceTier {
    Declared {
        index: usize,
    },
    Fallback {
        index: usize,
    },
}

Which TIER an instance was found in, and where inside it.

Lean tells you that an instance was synthesised; set_option trace.Meta.synthInstance tells you a search log you then have to read backwards. This names the winner’s coordinates directly, which is what a translator actually needs when two sources disagree about which instance a goal picked up.

Variants

Declared

An explicitly declared instance — Context::instances()[index].

Fields

index: usize

Fallback

A library/derived FALLBACK instance — Context::fallback_instances()[index].

Fields

index: usize

Trait Implementations

impl Clone for InstanceTier

fn clone(&self) -> InstanceTier

Returns a duplicate of the value.

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

Performs copy-assignment from source.

impl Debug for InstanceTier

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

Formats the value using the given formatter.

impl PartialEq for InstanceTier

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

impl StructuralPartialEq for InstanceTier