Struct RegularPracticalFragmentCheckResult 

pub struct RegularPracticalFragmentCheckResult {
    pub result: bool,
    pub reaches_communication: bool,
    pub well_formed: bool,
    pub full_unfold_head: String,
    pub reason: Option<String>,
}

Result of Lean regular-practical-fragment checking for a projected local type.

Fields

result: bool

Whether the local type is in the mechanically characterized fragment.

reaches_communication: bool

Whether full unfolding exposes a communication head.

well_formed: bool

Whether the local type is well formed on the Lean side.

full_unfold_head: String

Head constructor seen after full unfolding.

reason: Option<String>

Stable diagnostic reason when the type is outside the fragment.

Trait Implementations

impl Clone for RegularPracticalFragmentCheckResult

fn clone(&self) -> RegularPracticalFragmentCheckResult

Returns a duplicate of the value.

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

Performs copy-assignment from source.

impl Debug for RegularPracticalFragmentCheckResult

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

Formats the value using the given formatter.

impl PartialEq for RegularPracticalFragmentCheckResult

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

impl StructuralPartialEq for RegularPracticalFragmentCheckResult