Something went wrong. Try again.
forked from verus-lang/verus
Something went wrong. Try again.
123456789101112131415161718192021222324252627282930313233343536373839404142434445464748495051525354555657585960// rust_verify/tests/example.rsuse vstd::prelude::*;
verus! {
// ANCHOR: initialfn get_char() { let x = "hello world"; proof { reveal_strlit("hello world"); } assert(x@.len() == 11); let val = x.get_char(0); assert('h' == val);}// ANCHOR_END: initial
// ANCHOR: literal_eqfn literal_eq() { let x = "hello world"; let y = "hello world"; assert(x@ == y@);}// ANCHOR_END: literal_eq//// ANCHOR: literal_viewfn str_view() { let x = "hello world"; let ghost y: Seq<char> = x@;}// ANCHOR_END: literal_view
// ANCHOR: pre_substringfn subrange<'a>(s: &str) requires s@ =~= "Hello"@,{ proof { reveal_strlit("Hello"); reveal_strlit("H"); } assert(s@[..1] =~= "H"@);}// ANCHOR_END: pre_substring
// ANCHOR: substring_asciifn test() { let a = String::from_str(("ABC")); proof { reveal_strlit("ABC"); } assert(a.is_ascii()); let b = a.as_str().substring_ascii(2, 3); proof { reveal_strlit("C"); } assert(b@ =~= ("C")@);}// ANCHOR_END: substring_ascii
} // verus!