val application_value_size32: LSZ.size32 application_value_serializer
val application_value_size32: LSZ.size32 application_value_serializer
let application_value_size32 x = Size.application_value_size32 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

let application_value_bytesize x = Seq.length (spec_serializer_value x)

let application_value_bytesize_eq x = ()

// we need to add eta-expansions because the callees cannot be marked
// inline_for_extraction, since they are extern
/
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
LowParse.SLow.Base.size32 Zeta.Formats.Aux.Application_value.application_value_serializer
Zeta.Formats.Aux.Application_value.application_value Zeta.Formats.Aux.Application_value.Size.application_value_size32 FStar.UInt32.t LowParse.SLow.Base.size32_postcond Zeta.Formats.Aux.Application_value.application_value_parser_kind Zeta.Formats.Aux.Application_value.application_value_parser Zeta.Formats.Aux.Application_value.application_value_serializer
let application_value_size32 x =
  
Size.application_value_size32 x