pub trait ExecSpecOptionArrow<T>: Sized {
// Required methods
spec fn is_some_variant_spec(&self) -> bool;
exec fn exec_arrow_Some_0(&self) -> &T;
exec fn exec_arrow_0(&self) -> &T;
}Required Methods§
Sourcespec fn is_some_variant_spec(&self) -> bool
spec fn is_some_variant_spec(&self) -> bool
Sourceexec fn exec_arrow_Some_0(&self) -> &T
exec fn exec_arrow_Some_0(&self) -> &T
requires
self.is_some_variant_spec(),Sourceexec fn exec_arrow_0(&self) -> &T
exec fn exec_arrow_0(&self) -> &T
requires
self.is_some_variant_spec(),Dyn Compatibility§
This trait is not dyn compatible.
In older versions of Rust, dyn compatibility was called "object safety".
Implementations on Foreign Types§
Source§impl<T: DeepView> ExecSpecOptionArrow<T> for Option<T>
impl<T: DeepView> ExecSpecOptionArrow<T> for Option<T>
Source§open spec fn is_some_variant_spec(&self) -> bool
open spec fn is_some_variant_spec(&self) -> bool
{ *self is Some }Source§exec fn exec_arrow_Some_0(&self) -> res : &T
exec fn exec_arrow_Some_0(&self) -> res : &T
ensures
res.deep_view() == self.deep_view()->Some_0,Source§exec fn exec_arrow_0(&self) -> res : &T
exec fn exec_arrow_0(&self) -> res : &T
ensures
res.deep_view() == self.deep_view()->0,