val len_of_character_string (t: character_string_type) (x: datatype_of_asn1_type t)
    : Tot (asn1_value_int32_of_type t)
val len_of_character_string (t: character_string_type) (x: datatype_of_asn1_type t)
    : Tot (asn1_value_int32_of_type t)
let len_of_character_string
  (t: character_string_type)
  (x: datatype_of_asn1_type t)
: Tot (asn1_value_int32_of_type t)
= match t with
  | IA5_STRING -> dfst (x <: datatype_of_asn1_type IA5_STRING)
  | PRINTABLE_STRING -> dfst (x <: datatype_of_asn1_type PRINTABLE_STRING)
module ASN1.Spec.Value.CharacterString

open ASN1.Spec.Base
open LowParse.Spec.Bytes

open ASN1.Base
open ASN1.Spec.Tag
open ASN1.Spec.Length
include ASN1.Spec.Value.StringCombinator
include ASN1.Spec.Value.IA5_STRING
include ASN1.Spec.Value.PRINTABLE_STRING

open FStar.Integers

module B32 = FStar.Bytes

#set-options "--z3rlimit 32 --fuel 0 --ifuel 0"

(* ZT: I think we can leave this module exposed. *)
/
prims.fst.checked LowParse.Spec.Bytes.fst.checked FStar.Pervasives.fsti.checked FStar.Integers.fst.checked FStar.Bytes.fsti.checked ASN1.Spec.Value.StringCombinator.fsti.checked ASN1.Spec.Value.PRINTABLE_STRING.fsti.checked ASN1.Spec.Value.IA5_STRING.fsti.checked ASN1.Spec.Tag.fsti.checked ASN1.Spec.Length.fsti.checked ASN1.Spec.Base.fst.checked ASN1.Base.fst.checked
ASN1.Spec.Value.CharacterString.fst
t: ASN1.Base.character_string_type -> x: ASN1.Base.datatype_of_asn1_type t
  -> ASN1.Base.asn1_value_int32_of_type t
ASN1.Base.character_string_type ASN1.Base.datatype_of_asn1_type FStar.Pervasives.dfst ASN1.Base.asn1_value_int32_of_type ASN1.Base.IA5_STRING ASN1.Base.character_string_lbytes32 ASN1.Base.PRINTABLE_STRING
let len_of_character_string (t: character_string_type) (x: datatype_of_asn1_type t)
    : Tot (asn1_value_int32_of_type t) =
  
match t with
| IA5_STRING -> dfst (x <: datatype_of_asn1_type IA5_STRING)
| PRINTABLE_STRING -> dfst (x <: datatype_of_asn1_type PRINTABLE_STRING)