1use vstd::prelude::*;
2
3verus! {
4
5#[verifier::when_used_as_spec(as_ptr_spec)]
6pub assume_specification<T>[ <[T]>::as_ptr ](s: &[T]) -> (r: *const T)
7 ensures
8 r == as_ptr_spec(s),
9;
10
11pub uninterp spec fn as_ptr_spec<T>(s: &[T]) -> *const T;
12
13}