val length_of_opaque_serialization : s: LowParse.Spec.Base.serializer p -> x: t -> Prims.GTot Prims.nat
let length_of_opaque_serialization
  (#t: Type0)
  (#k: parser_kind)
  (#p: parser k t)
  (s: serializer p)
  (x: t)
= Seq.length (s `serialize` x)
module ASN1.Spec.Base

include LowParse.Spec.Base
include LowParse.Spec.Combinators

unfold
let coerce_parser_serializer
  (#t2: Type0)
  (#k: parser_kind)
  (#t1: Type0)
  (#p1: parser k t1)
  (p2: parser k t2)
  (s: serializer p1)
  (u: unit { t2 == t1 /\ p2 == coerce_parser t2 p1} )
: Tot (serializer (p2))
= s
/
prims.fst.checked LowParse.Spec.Combinators.fsti.checked LowParse.Spec.Base.fsti.checked FStar.Seq.fst.checked FStar.Pervasives.fsti.checked
ASN1.Spec.Base.fst
s: LowParse.Spec.Base.serializer p -> x: t -> Prims.GTot Prims.nat
LowParse.Spec.Base.parser_kind LowParse.Spec.Base.parser LowParse.Spec.Base.serializer FStar.Seq.Base.length LowParse.Bytes.byte LowParse.Spec.Base.serialize Prims.nat
let length_of_opaque_serialization
      (#t: Type0)
      (#k: parser_kind)
      (#p: parser k t)
      (s: serializer p)
      (x: t)
     =
  
Seq.length (s `serialize` x)