val filter_x509_version (x: datatype_of_asn1_type INTEGER) : GTot bool
val filter_x509_version (x: datatype_of_asn1_type INTEGER) : GTot bool
let filter_x509_version
  (x: datatype_of_asn1_type INTEGER)
: GTot bool
= 0l <= x && x <= 2l
module X509.BasicFields.Version

open LowParse.Low.Base

open ASN1.Spec
open ASN1.Low

open X509.Base

open FStar.Integers

#set-options "--z3rlimit 32 --fuel 0 --ifuel 0"
/
X509.Base.fst.checked prims.fst.checked LowParse.Low.Base.fst.checked FStar.UInt8.fsti.checked FStar.UInt32.fsti.checked FStar.Pervasives.fsti.checked FStar.Integers.fst.checked FStar.Int32.fsti.checked FStar.Classical.fsti.checked ASN1.Spec.fst.checked ASN1.Low.fst.checked
X509.BasicFields.Version.fsti
x: ASN1.Base.datatype_of_asn1_type ASN1.Base.INTEGER -> Prims.GTot Prims.bool
ASN1.Base.datatype_of_asn1_type ASN1.Base.INTEGER Prims.op_AmpAmp FStar.Integers.op_Less_Equals FStar.Integers.Signed FStar.Integers.W32 FStar.Int32.__int_to_t Prims.bool
let filter_x509_version (x: datatype_of_asn1_type INTEGER) : GTot bool =
  
0l <= x && x <= 2l