val serialize32_asn1_ASN1_NULL_backwards (_:unit)
: (serializer32_backwards serialize_asn1_ASN1_NULL)
val serialize32_asn1_ASN1_NULL_backwards (_:unit)
: (serializer32_backwards serialize_asn1_ASN1_NULL)
let serialize32_asn1_ASN1_NULL_backwards ()
= fun (_: datatype_of_asn1_type ASN1_NULL)
    (#rrel #rel: _)
    (b: B.mbuffer byte rrel rel)
    (pos: size_t)
-> 0ul
module ASN1.Low.Value.NULL

open ASN1.Base
open ASN1.Spec.Value.NULL
open ASN1.Low.Base

open FStar.Integers

module B = LowStar.Buffer

friend ASN1.Spec.Value.NULL

(* NOTE: Read after `ASN1.Spec.Tag`, `ASN1.Spec.Length` *)
/
prims.fst.checked LowStar.Buffer.fst.checked FStar.UInt32.fsti.checked FStar.Pervasives.Native.fst.checked FStar.Pervasives.fsti.checked FStar.Integers.fst.checked ASN1.Spec.Value.NULL.fst.checked ASN1.Spec.Value.NULL.fst.checked ASN1.Spec.Tag.fsti.checked ASN1.Spec.Length.fsti.checked ASN1.Low.Tag.fsti.checked ASN1.Low.Length.fsti.checked ASN1.Low.Base.fst.checked ASN1.Base.fst.checked
ASN1.Low.Value.NULL.fst
_: Prims.unit -> ASN1.Low.Base.serializer32_backwards ASN1.Spec.Value.NULL.serialize_asn1_ASN1_NULL
Prims.unit ASN1.Base.datatype_of_asn1_type ASN1.Base.ASN1_NULL LowStar.Monotonic.Buffer.srel ASN1.Low.Base.byte LowStar.Monotonic.Buffer.mbuffer ASN1.Low.Base.size_t FStar.UInt32.__uint_to_t FStar.UInt32.t
let serialize32_asn1_ASN1_NULL_backwards () =
  
fun
  (_: datatype_of_asn1_type ASN1_NULL)
  (#rrel: _)
  (#rel: _)
  (b: B.mbuffer byte rrel rel)
  (pos: size_t)
  ->
  0ul