valid_utf8_last

vstd::utf8

Function valid_utf8_last 

Source 
pub broadcast proof fn valid_utf8_last(s: Seq<u8>)
Expand description
requires
valid_utf8(s),
s.len() > 0,
ensures
!is_continuation_byte(s.last()) ==> is_leading_byte_width_1(s.last()),