val valid_keyPurposeIDs (oids: list (datatype_of_asn1_type OID)) : Type0
val valid_keyPurposeIDs (oids: list (datatype_of_asn1_type OID)) : Type0
let valid_keyPurposeIDs
  (oids: list (datatype_of_asn1_type OID))
: Type0
= 0 < List.length oids /\ (List.length oids) < 10
module X509.ExtFields.ExtendedKeyUsage

open LowParse.Spec.Base
open LowParse.Spec.Combinators

open ASN1.Base
open ASN1.Spec
open ASN1.Low

open X509.Base
open FStar.Integers
module B32 = FStar.Bytes

module T = FStar.Tactics
module P = FStar.Pervasives

(*
 * AR: TODO: this module has some scope for improvements
             it's hard to write an interface to hide defns, since a tactic requires those defns, I think *)

#set-options "--z3rlimit 32 --fuel 2 --ifuel 0"

(*
 * KeyPurposeIDs
 *)
/
X509.BasicFields.Extension2.fsti.checked X509.Base.fst.checked prims.fst.checked LowParse.Spec.Combinators.fsti.checked LowParse.Spec.Base.fsti.checked FStar.Tactics.fst.checked FStar.Seq.fst.checked FStar.Pervasives.Native.fst.checked FStar.Pervasives.fsti.checked FStar.List.Tot.Properties.fst.checked FStar.List.Tot.Base.fst.checked FStar.List.fst.checked FStar.Integers.fst.checked FStar.Classical.fsti.checked FStar.Bytes.fsti.checked ASN1.Spec.fst.checked ASN1.Low.fst.checked ASN1.Base.fst.checked
X509.ExtFields.ExtendedKeyUsage.fst
oids: Prims.list (ASN1.Base.datatype_of_asn1_type ASN1.Base.OID) -> Type0
Prims.list ASN1.Base.datatype_of_asn1_type ASN1.Base.OID Prims.l_and Prims.b2t FStar.Integers.op_Less FStar.Integers.Signed FStar.Integers.Winfinite FStar.List.Tot.Base.length
let valid_keyPurposeIDs (oids: list (datatype_of_asn1_type OID)) : Type0 =
  
0 < List.length oids /\ (List.length oids) < 10