vstd/std_specs/
char.rs

1use super::super::prelude::*;
2use super::super::utf8::encode_scalar;
3
4verus! {
5
6/// The byte width of `c`'s UTF-8 encoding, using the same scalar-value
7/// boundaries as [`encode_scalar`].
8#[verifier::allow_in_spec]
9pub assume_specification[ char::len_utf8 ](c: char) -> usize
10    returns
11        encode_scalar(c as u32).len() as usize,
12;
13
14/// Unicode's `White_Space` property:
15/// <https://www.unicode.org/reports/tr44/#White_Space>.
16pub open spec fn is_white_space(c: char) -> bool {
17    c == '\u{9}' || c == '\u{A}' || c == '\u{B}' || c == '\u{C}' || c == '\u{D}' || c == '\u{20}'
18        || c == '\u{85}' || c == '\u{A0}' || c == '\u{1680}' || c == '\u{2000}' || c == '\u{2001}'
19        || c == '\u{2002}' || c == '\u{2003}' || c == '\u{2004}' || c == '\u{2005}' || c
20        == '\u{2006}' || c == '\u{2007}' || c == '\u{2008}' || c == '\u{2009}' || c == '\u{200A}'
21        || c == '\u{2028}' || c == '\u{2029}' || c == '\u{202F}' || c == '\u{205F}' || c
22        == '\u{3000}'
23}
24
25pub assume_specification[ char::is_whitespace ](c: char) -> (res: bool)
26    returns
27        is_white_space(c),
28;
29
30} // verus!
vstd/std_specs/char.rs

vstd/std_specs/
char.rs
