Struct Diagnostic 

pub struct Diagnostic {
    pub code: DiagnosticCode,
    pub stage: &'static str,
    pub declaration: Option<String>,
    pub line: Option<usize>,
    pub message: String,
    /* private fields */
}

One typed, located diagnostic of a result.

Fields

code: DiagnosticCode

stage: &'static str

The receipt stage it concerns.

declaration: Option<String>

The Lean declaration (dotted name) it concerns.

line: Option<usize>

The 1-based line of the input it concerns.

message: String

Implementations

impl Diagnostic

pub fn new( stage: &'static str, code: DiagnosticCode, message: impl Into<String>, ) -> Self

A diagnostic of a classified code. An unclassified or usage code is an unsupported feature.

pub fn of_refusal(stage: &'static str, verdict: &Verdict) -> Self

The diagnostic a refusal carries, with its location.

pub fn with_declaration(self, declaration: impl Into<String>) -> Self

pub fn with_line(self, line: usize) -> Self

pub fn outcome(&self) -> Outcome

The outcome this diagnostic decides when its stage is the first that did not pass.

pub fn to_json(&self) -> Value

Trait Implementations

impl Clone for Diagnostic

fn clone(&self) -> Diagnostic

Returns a duplicate of the value.

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

Performs copy-assignment from source.

impl Debug for Diagnostic

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

Formats the value using the given formatter.

impl PartialEq for Diagnostic

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

impl StructuralPartialEq for Diagnostic