Merge pull request #1827 from verus-lang/option-view-export

Move View and DeepView impls of Option to vstd::view

Author: zhengyao-lin

source/vstd/std_specs/option.rs

@@ -7,25 +7,6 @@ use core::option::Option::Some;
 
 verus! {
 
-impl<T> View for Option<T> {
-    type V = Option<T>;
-
-    open spec fn view(&self) -> Option<T> {
-        *self
-    }
-}
-
-impl<T: DeepView> DeepView for Option<T> {
-    type V = Option<T::V>;
-
-    open spec fn deep_view(&self) -> Option<T::V> {
-        match self {
-            Some(t) => Some(t.deep_view()),
-            None => None,
-        }
-    }
-}
-
 ////// Add is_variant-style spec functions
 pub trait OptionAdditionalFns<T>: Sized {
     #[deprecated(note = "is_Variant is deprecated - use `->` or `matches` instead: https://verus-lang.github.io/verus/guide/datatypes_enum.html")]

source/vstd/view.rs

@@ -134,6 +134,25 @@ impl<T: DeepView> DeepView for alloc::vec::Vec<T> {
     }
 }
 
+impl<T> View for Option<T> {
+    type V = Option<T>;
+
+    open spec fn view(&self) -> Option<T> {
+        *self
+    }
+}
+
+impl<T: DeepView> DeepView for Option<T> {
+    type V = Option<T::V>;
+
+    open spec fn deep_view(&self) -> Option<T::V> {
+        match self {
+            Some(t) => Some(t.deep_view()),
+            None => None,
+        }
+    }
+}
+
 macro_rules! declare_identity_view {
     ($t:ty) => {
         #[cfg_attr(verus_keep_ghost, verifier::verify)]