Enum Value 

pub enum Value<T, B: BoundaryKind = GenericBoundary> {
    Origin(B),
    Boundary {
        reason: B,
        last: T,
    },
    Contents(T),
}

The core type. Origin, Boundary, or Contents. Three sorts. Every domain.

Formally verified in Lean 4 as Val α:

• origin — absorbs everything (I1, I2, I3)
• container — structural, preserves last known value
• contents — actual arithmetic, the field interior

508 theorems. Zero errors. Zero sorries.

Variants

Origin(B)

Origin: the computation hit the absolute boundary. There is no last value. The reason is all that exists. The ocean absorbed the fish.

Boundary

Boundary: the computation crossed an edge. Carries the reason and the last known value. The container preserves what was there.

Fields

reason: B

last: T

Contents(T)

Contents: the value is in safe territory. Arithmetic lives here.

Implementations

impl<T, B: BoundaryKind> Value<T, B>

pub fn origin(reason: B) -> Self

Construct an origin value — pure boundary, no last value.

pub fn boundary(reason: B, last: T) -> Self

Construct a boundary value with a reason and last known value.

pub fn contents(value: T) -> Self

Construct a contents value.

pub fn is_contents(&self) -> bool

pub fn is_origin(&self) -> bool

pub fn is_boundary(&self) -> bool

pub fn or(self, fallback: T) -> T

Unwrap the contents value, or return a fallback.

Both Origin and Boundary return the fallback — if you need to distinguish them, use match or or_else instead.

pub fn or_else( self, on_boundary: impl FnOnce(B, T) -> T, on_origin: impl FnOnce(B) -> T, ) -> T

Handle Origin and Boundary distinctly when extracting a value.

Unlike or, this preserves the distinction between the three sorts:

• Contents: returns the value directly
• Boundary: calls on_boundary with the reason AND last value
• Origin: calls on_origin with only the reason (no last value)

pub fn unwrap(self) -> T

Unwrap the contents value, or panic.

pub fn map<U>(self, f: impl FnOnce(T) -> U) -> Value<U, B>

Map over the contents value. Origin passes through unchanged. Boundary maps the transform over last.

Note: if you chain multiple map calls, last reflects the transformed value at each step, not the original value at the boundary. If you need the original last, use match explicitly.

pub fn propagate(self) -> Result<T, B>

Extract the contents value, or return the boundary reason as Err for ? propagation.

Both Boundary and Origin become Err(reason). The last value in Boundary is dropped. If you need last, use match or propagate_with_last instead.

pub fn propagate_with_last(self) -> Result<T, (B, Option<T>)>

Propagate, preserving the last value if at a Boundary.

• Contents → Ok(value)
• Boundary → Err((reason, Some(last)))
• Origin → Err((reason, None))

pub fn trace(self, chain: &mut Chain, label: &'static str) -> Result<T, B>

where T: Debug,

Extract the contents value while recording the step in a trace.

pub fn and_then<U>(self, f: impl FnOnce(T) -> Value<U, B>) -> Value<U, B>

Chain operations that may themselves hit a boundary.

If already at Origin, propagates as Origin. If at Boundary, last is dropped and propagates as Origin — because the type has changed and the old last has no meaning in the new type. If you need last, use match before chaining.

and_then is for Contents pipelines. For Boundary-aware chaining, use match explicitly. No Default bound needed — Origin carries no value.

Trait Implementations

impl<T: Debug, B: Debug + BoundaryKind> Debug for Value<T, B>

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

Formats the value using the given formatter.