Struct NativeDecision 

pub struct NativeDecision {
    pub leaf: usize,
    pub premise: usize,
    pub appeal: usize,
    pub evaluation: usize,
    pub proposition: usize,
    pub instance: usize,
    pub decision: String,
}

One recognized leaf: Lean’s appeal to its compiler, and the pieces its re-derivation keeps.

Fields

leaf: usize

The leaf, of_decide_eq_true p inst (Lean.ofReduceBool d Bool.true h).

premise: usize

of_decide_eq_true p inst, which the re-derived leaf keeps.

appeal: usize

Lean’s appeal, Lean.ofReduceBool d Bool.true h, which the re-derived leaf drops.

evaluation: usize

h = Eq.refl.{1} Bool Bool.true, the proof of Decidable.decide p inst = Bool.true the re-derived leaf supplies directly.

proposition: usize

The proposition p.

instance: usize

Its decision procedure inst : Decidable p.

decision: String

The constant Lean compiled and evaluated, as Lean writes its name.

Implementations

impl NativeDecision

pub fn to_json(&self) -> Value

Trait Implementations

impl Clone for NativeDecision

fn clone(&self) -> NativeDecision

Returns a duplicate of the value.

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

Performs copy-assignment from source.

impl Debug for NativeDecision

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

Formats the value using the given formatter.

impl PartialEq for NativeDecision

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

impl StructuralPartialEq for NativeDecision