Struct VerifyCaseResult 

pub struct VerifyCaseResult {
    pub outcome: VerifyCaseOutcome,
    pub span: Option<SourceSpan>,
    pub case_expr: String,
    pub case_index: usize,
    pub case_total: usize,
    pub law_context: Option<VerifyLawContext>,
    pub from_hostile: bool,
    pub hostile_profile: Option<String>,
}

Fields

outcome: VerifyCaseOutcome

span: Option<SourceSpan>

case_expr: String

case_index: usize

case_total: usize

law_context: Option<VerifyLawContext>

from_hostile: bool

true for cases injected by aver verify --hostile boundary expansion (a binding the user did not declare). Drives differential reporting: a hostile-only failure means the claim is not universal, so it isn’t a law — either encode the missing precondition with when, or downgrade from law form to verify (cases form, example/scenario semantics) with the values you actually meant.

hostile_profile: Option<String>

Display label for the effect-side hostile profile, e.g. "Time.now/frozen + Random.int/min". None when the case wasn’t effect-hostile-expanded (declared, value-hostile-only, or fns without applicable classified effects). Reporting prepends this to the diagnostic so the user sees which adversarial world broke the law: “Time.now/frozen + Random.int/min: assumed deadline > now”.

Trait Implementations

impl Clone for VerifyCaseResult

fn clone(&self) -> VerifyCaseResult

Returns a duplicate of the value.

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

Performs copy-assignment from source.

impl Debug for VerifyCaseResult

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

Formats the value using the given formatter.