Struct InstanceChoice 

pub struct InstanceChoice {
    pub value: Term,
    pub tier: InstanceTier,
    pub priority: i64,
    pub considered: Vec<InstanceProbe>,
    pub pruned: usize,
}

A resolved instance together with WHY it won — the audit trail Lean’s instance resolution does not expose.

considered lists, in the exact order they were tried, every candidate the search touched before settling: (tier, priority, whether it applied). A candidate that applied but lost (an ambiguous hierarchy diamond) is therefore distinguishable from one that never matched, which is the distinction that makes an “unexpected instance” bug findable.

Fields

value: Term

The instance term, with its metavariables instantiated — exactly what resolve_instance returns.

tier: InstanceTier

Where the winner came from.

priority: i64

Its priority (Lean’s default, 1000, unless declared otherwise). Fallback entries carry no priority of their own — the tier itself is the ranking — and report the default.

considered: Vec<InstanceProbe>

Every candidate the search touched, in the order it touched them.

pruned: usize

How many declared instances the DISCRIMINATION INDEX excluded before any of them was tried — see Context::instance_search_order_for.

Lean’s getUnify hands back the surviving entries and throws this number away, so “why was my instance never tried?” has no answer there short of reading a trace log backwards. Here it is a field: considered.len() + pruned is the whole database.

Trait Implementations

impl Clone for InstanceChoice

fn clone(&self) -> InstanceChoice

Returns a duplicate of the value.

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

Performs copy-assignment from source.

impl Debug for InstanceChoice

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

Formats the value using the given formatter.