Struct BmpStringSpec 

pub struct BmpStringSpec {
    pub inner: Seq<char>,
}

Fields

inner: Seq<char>

Implementations

impl BmpStringSpec

pub open spec fn wf(&self) -> bool

{ is_valid_bmp_chars(self.inner) }

Trait Implementations

impl<const HAS_MIN: bool, const MIN: usize, const HAS_MAX: bool, const MAX: usize> SpecPred<BmpStringSpec> for Size<HAS_MIN, MIN, HAS_MAX, MAX>

open spec fn apply(&self, value: BmpStringSpec) -> bool

{ size_in_range::<HAS_MIN, MIN, HAS_MAX, MAX>(value.inner.len()) }