val inbound_envelop_tag_with_value_of : a: ASN1.Base.asn1_tag_t -> s: LowParse.Spec.Base.serializer p -> Type0
let inbound_envelop_tag_with_value_of
  (#k: parser_kind)
  (#t: Type0)
  (#p: parser k t)
  (a: asn1_tag_t)
  (s: serializer p)
= x: t{ asn1_value_length_inbound_of_type a (length_of_opaque_serialization s x) }
module ASN1.Spec.Value.Envelop

open ASN1.Base
open ASN1.Spec.Base
open ASN1.Spec.Tag
open ASN1.Spec.Length
open LowParse.Spec.FLData

open FStar.Integers

(* NOTE: Read after `ASN1.Spec.Tag`, `ASN1.Spec.Length`, `ASN1.Spec.Value.*` *)

(* NOTE: Use `parse_fldata_strong` to construct fixed-length parsers (with the strong prefix proeprty),
         where these fixed-length is runtimely parsed.
 *)

// unfold
/
prims.fst.checked LowParse.Spec.FLData.fst.checked FStar.Seq.fst.checked FStar.Pervasives.Native.fst.checked FStar.Pervasives.fsti.checked FStar.Integers.fst.checked ASN1.Spec.Tag.fsti.checked ASN1.Spec.Length.fsti.checked ASN1.Spec.Base.fst.checked ASN1.Base.fst.checked
ASN1.Spec.Value.Envelop.fsti
a: ASN1.Base.asn1_tag_t -> s: LowParse.Spec.Base.serializer p -> Type0
LowParse.Spec.Base.parser_kind LowParse.Spec.Base.parser ASN1.Base.asn1_tag_t LowParse.Spec.Base.serializer Prims.b2t ASN1.Base.asn1_value_length_inbound_of_type ASN1.Spec.Base.length_of_opaque_serialization
let inbound_envelop_tag_with_value_of
      (#k: parser_kind)
      (#t: Type0)
      (#p: parser k t)
      (a: asn1_tag_t)
      (s: serializer p)
     =
  
x: t{asn1_value_length_inbound_of_type a (length_of_opaque_serialization s x)}