Struct PrintableStringSpec 

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

Fields

inner: Seq<char>

Implementations

impl PrintableStringSpec

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

{ is_valid_printable_string_spec(vstd::utf8::encode_utf8(self.inner)) }

Trait Implementations

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

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

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

impl SpecPred<PrintableStringSpec> for NumericStringChars

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

{ is_valid_numeric_string(value.inner) }