Skip to main content

vstd_extra/external/
convert.rs

1use vstd::prelude::*;
2
3use core::marker::PointeeSized;
4
5verus! {
6
7#[verifier::external_trait_specification]
8#[verifier::external_trait_extension(AsRefSpec via AsRefSpecImpl)]
9pub trait ExAsRef<T: PointeeSized>: PointeeSized {
10    type ExternalTraitSpecificationFor: core::convert::AsRef<T>;
11
12    spec fn as_ref_spec(&self) -> &T;
13
14    spec fn obeys_as_ref_spec() -> bool;
15
16    fn as_ref(&self) -> (r: &T)
17        ensures
18            Self::obeys_as_ref_spec() ==> r == self.as_ref_spec(),
19    ;
20}
21
22} // verus!