Struct RuleProvenance 

pub struct RuleProvenance {
    pub rule_id: String,
    pub head: String,
    pub source_kind: RuleSourceKind,
    pub source_span: Option<String>,
    pub generation_trace_hash: Option<String>,
    pub support_relation_ids: Vec<String>,
    pub counterexample_relation_ids: Vec<String>,
}

Public rule provenance record.

Fields

rule_id: String

Stable rule identifier within the diagnostic report.

head: String

Formatted rule head, e.g. reach(X, Y).

source_kind: RuleSourceKind

Rule origin class.

source_span: Option<String>

Source span when available from the parser.

generation_trace_hash: Option<String>

Stable hash of the source or generation trace.

support_relation_ids: Vec<String>

Body relation ids that support this rule.

counterexample_relation_ids: Vec<String>

Counterexample relation ids when supplied by an induction path.

Trait Implementations

impl Clone for RuleProvenance

fn clone(&self) -> RuleProvenance

Returns a duplicate of the value.

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

Performs copy-assignment from source.

impl Debug for RuleProvenance

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

Formats the value using the given formatter.

impl PartialEq for RuleProvenance

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

impl StructuralPartialEq for RuleProvenance