Struct Ia5StringSpec 

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

Fields

inner: Seq<char>

Implementations

impl Ia5StringSpec

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

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

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

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