val synth_asn1_ia5_string
      (len: asn1_value_int32_of_type IA5_STRING)
      (s32: parse_filter_refine (filter_asn1_ia5_string len))
    : GTot (value: datatype_of_asn1_type IA5_STRING {(dfst value) == len})
val synth_asn1_ia5_string
      (len: asn1_value_int32_of_type IA5_STRING)
      (s32: parse_filter_refine (filter_asn1_ia5_string len))
    : GTot (value: datatype_of_asn1_type IA5_STRING {(dfst value) == len})
let synth_asn1_ia5_string
  (len: asn1_value_int32_of_type IA5_STRING)
  (s32: parse_filter_refine (filter_asn1_ia5_string len))
: GTot (value: datatype_of_asn1_type IA5_STRING{(dfst value) == len})
= (|len, s32|)
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

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
/
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:
      LowParse.Spec.Combinators.parse_filter_refine (ASN1.Spec.Value.IA5_STRING.filter_asn1_ia5_string
            len)
  -> Prims.GTot
    (value:
      ASN1.Base.datatype_of_asn1_type ASN1.Base.IA5_STRING {FStar.Pervasives.dfst value == len})
ASN1.Base.asn1_value_int32_of_type ASN1.Base.IA5_STRING LowParse.Spec.Combinators.parse_filter_refine FStar.Bytes.lbytes32 ASN1.Spec.Value.IA5_STRING.filter_asn1_ia5_string Prims.Mkdtuple2 ASN1.Base.character_string_lbytes32 ASN1.Base.datatype_of_asn1_type Prims.eq2 FStar.Pervasives.dfst
let synth_asn1_ia5_string
      (len: asn1_value_int32_of_type IA5_STRING)
      (s32: parse_filter_refine (filter_asn1_ia5_string len))
    : GTot (value: datatype_of_asn1_type IA5_STRING {(dfst value) == len}) =
  
(| len, s32 |)