Struct TeletexStringSpec 

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

Fields

inner: Seq<char>

Implementations

impl TeletexStringSpec

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

{ is_valid_teletex_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<TeletexStringSpec> for Size<HAS_MIN, MIN, HAS_MAX, MAX>

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

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