Enum Verdict 

pub enum Verdict {
    Reject(Reason),
    Decline(Reason),
}

The kernel’s decision on an input it did not accept. Reject: the input is wrong. Decline: the input may be right, but this reader does not accept it (and never approximates it).

Variants

Reject(Reason)

Decline(Reason)

Implementations

impl Verdict

pub fn reason(&self) -> &Reason

pub fn code(&self) -> i32

The benchmark protocol’s exit code: 1 for a rejection, 2 for a decline.

pub fn outcome(&self) -> Outcome

The logos-lean-result/1 outcome this refusal decides.

pub fn at_line(self, line: usize) -> Verdict

The same verdict, recorded as arising at 1-based input line (the innermost line wins).

pub fn in_declaration(self, name: impl Into<String>) -> Verdict

The same verdict, recorded as arising in the Lean declaration name (the innermost wins).

Trait Implementations

impl Debug for Verdict

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

Formats the value using the given formatter.

impl From<KernelError> for Verdict

fn from(error: KernelError) -> Self

Converts to this type from the input type.