vest_lib/regular/
clone.rs

1use super::bytes::{Fixed, Tail, Variable};
2use super::uints::{U16Le, U32Le, U64Le, U8};
3use vstd::prelude::*;
4
5verus! {
6
7macro_rules! impl_reflexive_clone {
8    ($($ty:ty),*) => {
9        ::vstd::prelude::verus! {
10            $(
11                impl Clone for $ty {
12                    fn clone(&self) -> (out: Self)
13                        ensures
14                            out == *self,
15                    {
16                        Self
17                    }
18                }
19            )*
20        }
21    };
22}
23
24impl_reflexive_clone!(U8, U16Le, U32Le, U64Le, Tail);
25
26impl Clone for Variable {
27    fn clone(&self) -> (out: Self)
28        ensures
29            out == *self,
30    {
31        Variable(self.0)
32    }
33}
34
35impl<const N: usize> Clone for Fixed<N> {
36    fn clone(&self) -> (out: Self)
37        ensures
38            out == *self,
39    {
40        Fixed
41    }
42}
43
44} // verus!
vest_lib/regular/clone.rs

vest_lib/regular/
clone.rs
