val application_value_bytesize (x:application_value) : GTot nat
val application_value_bytesize (x:application_value) : GTot nat
let application_value_bytesize x = Seq.length (spec_serializer_value x)
module Zeta.Formats.Aux.Application_value

friend Zeta.Formats.Aux.External.App
open Zeta.Steel.ApplicationTypes
open Zeta.Formats.Lib

module Spec = Zeta.Formats.Aux.Application_value.Spec
module Size = Zeta.Formats.Aux.Application_value.Size
module Low = Zeta.Formats.Aux.Application_value.Low

let application_value_parser = Spec.application_value_parser

let application_value_serializer = Spec.application_value_serializer
/
Zeta.Steel.ApplicationTypes.fsti.checked Zeta.Formats.Lib.fst.checked Zeta.Formats.Aux.External.App.fst.checked Zeta.Formats.Aux.Application_value.Spec.fst.checked Zeta.Formats.Aux.Application_value.Size.fsti.checked Zeta.Formats.Aux.Application_value.Low.fsti.checked prims.fst.checked FStar.Seq.fst.checked FStar.Pervasives.fsti.checked
Zeta.Formats.Aux.Application_value.fst
x: Zeta.Formats.Aux.Application_value.application_value -> Prims.GTot Prims.nat
Zeta.Formats.Aux.Application_value.application_value FStar.Seq.Base.length Zeta.Steel.Parser.byte Zeta.Steel.ApplicationTypes.spec_serializer_value Prims.nat
let application_value_bytesize x =
  
Seq.length (spec_serializer_value x)