Enum IncompleteKind 

pub enum IncompleteKind {
    Unsupported,
    ResourceLimit {
        steps: usize,
        depth: usize,
        nodes: usize,
    },
}

What stopped the independent kernel.

Variants

Unsupported

A construct outside the covered fragment: a Hole (an unelaborated metavariable), a match on an inductive whose head this kernel does not recognize, or a reduction rule of the first kernel that this one does not compute. More resources cannot decide it.

ResourceLimit

One of this kernel’s resource bounds stopped the check before it decided: its reduction step budget, its nesting depth, its term size, its share of the native stack, or its input admission bounds. The bounds in force are recorded; more of the resource could decide it.

Fields

steps: usize

depth: usize

nodes: usize

Trait Implementations

impl Clone for IncompleteKind

fn clone(&self) -> IncompleteKind

Returns a duplicate of the value.

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

Performs copy-assignment from source.

impl Debug for IncompleteKind

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

Formats the value using the given formatter.

impl PartialEq for IncompleteKind

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

impl Eq for IncompleteKind

impl StructuralPartialEq for IncompleteKind