pub enum BlockerCode {
ProofMissingLemma,
ProofShapeMismatch,
ModelGap,
ImplDivergence,
ToolchainFailure,
ExternalDependency,
}Expand description
Deterministic blocker taxonomy codes.
Variants§
ProofMissingLemma
Missing helper lemma(s) or dependency theorem(s).
ProofShapeMismatch
Proof shape/tactic path mismatch after model evolution.
ModelGap
Lean model/spec is incomplete or inconsistent with intended semantics.
ImplDivergence
Rust runtime behavior diverges from formal model assumptions.
ToolchainFailure
CI/build/toolchain infrastructure prevents validation.
ExternalDependency
External dependency or sequencing blocker.
Trait Implementations§
Source§impl Clone for BlockerCode
impl Clone for BlockerCode
Source§fn clone(&self) -> BlockerCode
fn clone(&self) -> BlockerCode
Returns a duplicate of the value. Read more
1.0.0 · Source§fn clone_from(&mut self, source: &Self)
fn clone_from(&mut self, source: &Self)
Performs copy-assignment from
source. Read moreSource§impl Debug for BlockerCode
impl Debug for BlockerCode
Source§impl<'de> Deserialize<'de> for BlockerCode
impl<'de> Deserialize<'de> for BlockerCode
Source§fn deserialize<__D>(__deserializer: __D) -> Result<Self, __D::Error>where
__D: Deserializer<'de>,
fn deserialize<__D>(__deserializer: __D) -> Result<Self, __D::Error>where
__D: Deserializer<'de>,
Deserialize this value from the given Serde deserializer. Read more
Source§impl PartialEq for BlockerCode
impl PartialEq for BlockerCode
Source§impl Serialize for BlockerCode
impl Serialize for BlockerCode
impl Copy for BlockerCode
impl Eq for BlockerCode
impl StructuralPartialEq for BlockerCode
Auto Trait Implementations§
impl Freeze for BlockerCode
impl RefUnwindSafe for BlockerCode
impl Send for BlockerCode
impl Sync for BlockerCode
impl Unpin for BlockerCode
impl UnsafeUnpin for BlockerCode
impl UnwindSafe for BlockerCode
Blanket Implementations§
Source§impl<T> BorrowMut<T> for Twhere
T: ?Sized,
impl<T> BorrowMut<T> for Twhere
T: ?Sized,
Source§fn borrow_mut(&mut self) -> &mut T
fn borrow_mut(&mut self) -> &mut T
Mutably borrows from an owned value. Read more