val length_of_aliasKeyTBS_extensions_basicConstraints: Prims.unit
  -> GTot (asn1_TLV_length_of_type SEQUENCE)
val length_of_aliasKeyTBS_extensions_basicConstraints: Prims.unit
  -> GTot (asn1_TLV_length_of_type SEQUENCE)
let length_of_aliasKeyTBS_extensions_basicConstraints ()
: GTot (asn1_TLV_length_of_type SEQUENCE)
= length_of_x509_basicConstraints aliasKeyTBS_extensions_basicConstraints_isCA
module L0.X509.AliasKeyTBS.Extensions.BasicConstraints

open ASN1.Spec
open ASN1.Low
open X509
open FStar.Integers

module B32 = FStar.Bytes

#set-options "--z3rlimit 64 --fuel 0 --ifuel 0"

noextract inline_for_extraction
let aliasKeyTBS_extensions_basicConstraints_isCA: bool = false

let aliasKeyTBS_extensions_basicConstraints_t: Type
= x509_basicConstraints_t aliasKeyTBS_extensions_basicConstraints_isCA

let parse_aliasKeyTBS_extensions_basicConstraints
// : parser parse_x509_extension_kind aliasKeyTBS_extensions_basicConstraints_t
= aliasKeyTBS_extensions_basicConstraints_t
  `coerce_parser`
  parse_x509_basicConstraints aliasKeyTBS_extensions_basicConstraints_isCA

let serialize_aliasKeyTBS_extensions_basicConstraints
: serializer parse_aliasKeyTBS_extensions_basicConstraints
= coerce_parser_serializer
    (parse_aliasKeyTBS_extensions_basicConstraints)
    (serialize_x509_basicConstraints aliasKeyTBS_extensions_basicConstraints_isCA)
    ()

//noextract inline_for_extraction
let serialize32_aliasKeyTBS_extensions_basicConstraints_backwards
: serializer32_backwards serialize_aliasKeyTBS_extensions_basicConstraints
= coerce_serializer32_backwards
    (serialize_aliasKeyTBS_extensions_basicConstraints)
    (serialize32_x509_basicConstraints_backwards aliasKeyTBS_extensions_basicConstraints_isCA)
    ()
/
X509.fst.checked prims.fst.checked FStar.Pervasives.fsti.checked FStar.Integers.fst.checked FStar.Bytes.fsti.checked ASN1.Spec.fst.checked ASN1.Low.fst.checked
L0.X509.AliasKeyTBS.Extensions.BasicConstraints.fst
_: Prims.unit -> Prims.GTot (ASN1.Base.asn1_TLV_length_of_type ASN1.Base.SEQUENCE)
Prims.unit X509.ExtFields.BasicConstraints.length_of_x509_basicConstraints L0.X509.AliasKeyTBS.Extensions.BasicConstraints.aliasKeyTBS_extensions_basicConstraints_isCA ASN1.Base.asn1_TLV_length_of_type ASN1.Base.SEQUENCE
let length_of_aliasKeyTBS_extensions_basicConstraints () : GTot (asn1_TLV_length_of_type SEQUENCE) =
  
length_of_x509_basicConstraints aliasKeyTBS_extensions_basicConstraints_isCA