val application_value_jumper: LL.jumper application_value_parser
val application_value_jumper: LL.jumper application_value_parser
let application_value_jumper input pos = Low.application_value_jumper input pos
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

let application_value_size32 x = Size.application_value_size32 x

let application_value_validator input pos = Low.application_value_validator input pos
/
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.Low.Base.jumper Zeta.Formats.Aux.Application_value.application_value_parser
LowParse.Slice.srel LowParse.Bytes.byte LowParse.Slice.slice FStar.UInt32.t Zeta.Formats.Aux.Application_value.Low.application_value_jumper
let application_value_jumper input pos =
  
Low.application_value_jumper input pos