Trait UnwrapOrPanic 

pub trait UnwrapOrPanic: Sized {
    type Inner;

    // Required methods
    spec fn is_present(&self) -> bool;
    spec fn payload(&self) -> Self::Inner;
    exec fn unwrap_or_panic(self) -> r : Self::Inner;
}

Extension trait providing a panicking unwrap that models Rust’s real Option::unwrap semantics.

Verus’ Option::unwrap carries a requires self is Some; Rust’s unwrap instead panics on None. unwrap_or_panic diverges on None (via panic_diverge) — a sound model of the real panic — and discharges is_present() (i.e. self is Some for Option) at the call site by branch elimination, so callers need not prove the value is populated.

Required Associated Types

type Inner

Required Methods

spec fn is_present(&self) -> bool

spec fn payload(&self) -> Self::Inner

exec fn unwrap_or_panic(self) -> r : Self::Inner

requires

!self.is_present() ==> may_panic(),

ensures

self.is_present(),

r == self.payload(),

Dyn Compatibility

This trait is not dyn compatible.

In older versions of Rust, dyn compatibility was called "object safety".

Implementations on Foreign Types

impl<T> UnwrapOrPanic for Option<T>

open spec fn is_present(&self) -> bool

{ self is Some }

open spec fn payload(&self) -> T

{ self->0 }

exec fn unwrap_or_panic(self) -> r : T

type Inner = T

Implementors