val filter_asn1_ia5_string (len: asn1_value_int32_of_type IA5_STRING) (s32: B32.lbytes32 len)
    : GTot (bool)
val filter_asn1_ia5_string (len: asn1_value_int32_of_type IA5_STRING) (s32: B32.lbytes32 len)
    : GTot (bool)
let filter_asn1_ia5_string
  (len: asn1_value_int32_of_type IA5_STRING)
  (s32: B32.lbytes32 len)
: GTot (bool)
= let s = B32.reveal s32 in
  Seq.for_all valid_IA5_byte s
module ASN1.Spec.Value.IA5_STRING

open ASN1.Spec.Base

open ASN1.Base
open ASN1.Spec.Value.StringCombinator

open FStar.Integers

module B32 = FStar.Bytes
/
prims.fst.checked FStar.Seq.fst.checked FStar.Pervasives.fsti.checked FStar.Integers.fst.checked FStar.Bytes.fsti.checked ASN1.Spec.Value.StringCombinator.fsti.checked ASN1.Spec.Base.fst.checked ASN1.Base.fst.checked
ASN1.Spec.Value.IA5_STRING.fsti
len: ASN1.Base.asn1_value_int32_of_type ASN1.Base.IA5_STRING -> s32: FStar.Bytes.lbytes32 len
  -> Prims.GTot Prims.bool
ASN1.Base.asn1_value_int32_of_type ASN1.Base.IA5_STRING FStar.Bytes.lbytes32 FStar.Seq.Properties.for_all FStar.Bytes.byte ASN1.Base.valid_IA5_byte FStar.Seq.Base.seq FStar.UInt8.t FStar.Bytes.reveal Prims.bool
let filter_asn1_ia5_string (len: asn1_value_int32_of_type IA5_STRING) (s32: B32.lbytes32 len)
    : GTot (bool) =
  
let s = B32.reveal s32 in
Seq.for_all valid_IA5_byte s