Enum PreservationProof 

pub enum PreservationProof {
    IntCountdownLiteralZero,
}

Marker that the lowerer constructed a proof of preservation (recursive args stay in the precondition’s domain). The variants describe HOW the proof was constructed so future maintainers can trace why a given shape was accepted as native.

Variants

IntCountdownLiteralZero

match p { 0 -> base; _ -> rec(p-1, ...) } under p ≥ 0 precondition. Wildcard arm gives p ≠ 0, combined with p ≥ 0 yields p ≥ 1, so p - 1 ≥ 0.

Trait Implementations

impl Clone for PreservationProof

fn clone(&self) -> PreservationProof

Returns a duplicate of the value.

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

Performs copy-assignment from source.

impl Debug for PreservationProof

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

Formats the value using the given formatter.