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;
}Expand description
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§
Required Methods§
Sourcespec fn is_present(&self) -> bool
spec fn is_present(&self) -> bool
Sourceexec fn unwrap_or_panic(self) -> r : Self::Inner
exec fn unwrap_or_panic(self) -> r : Self::Inner
requires
!self.is_present() ==> may_panic(),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", so this trait is not object safe.