def commandDeclare_decidable_int_quantifiers__ : Lean.ParserDescr

@[instance_reducible]

instance Int8.instDecidableExists (P : Int8 → Prop) [DecidablePred P] : Decidable (∃ (x : Int8), P x)

theorem Int8.forall_iff_forall_ofBitVec {P : Int8 → Prop} : (∀ (x : Int8), P x) ↔ ∀ (x : BitVec 8), P (ofBitVec x)

theorem Int8.exists_iff_exists_ofBitVec {P : Int8 → Prop} : (∃ (x : Int8), P x) ↔ ∃ (x : BitVec 8), P (ofBitVec x)

@[instance_reducible]

instance Int8.instDecidableForall (P : Int8 → Prop) [DecidablePred P] : Decidable (∀ (x : Int8), P x)

theorem Int16.forall_iff_forall_ofBitVec {P : Int16 → Prop} : (∀ (x : Int16), P x) ↔ ∀ (x : BitVec 16), P (ofBitVec x)

theorem Int16.exists_iff_exists_ofBitVec {P : Int16 → Prop} : (∃ (x : Int16), P x) ↔ ∃ (x : BitVec 16), P (ofBitVec x)

@[instance_reducible]

instance Int16.instDecidableForall (P : Int16 → Prop) [DecidablePred P] : Decidable (∀ (x : Int16), P x)

@[instance_reducible]

instance Int16.instDecidableExists (P : Int16 → Prop) [DecidablePred P] : Decidable (∃ (x : Int16), P x)

theorem Int32.forall_iff_forall_ofBitVec {P : Int32 → Prop} : (∀ (x : Int32), P x) ↔ ∀ (x : BitVec 32), P (ofBitVec x)

theorem Int32.exists_iff_exists_ofBitVec {P : Int32 → Prop} : (∃ (x : Int32), P x) ↔ ∃ (x : BitVec 32), P (ofBitVec x)

@[instance_reducible]

instance Int32.instDecidableExists (P : Int32 → Prop) [DecidablePred P] : Decidable (∃ (x : Int32), P x)

@[instance_reducible]

instance Int32.instDecidableForall (P : Int32 → Prop) [DecidablePred P] : Decidable (∀ (x : Int32), P x)

@[instance_reducible]

instance Int64.instDecidableExists (P : Int64 → Prop) [DecidablePred P] : Decidable (∃ (x : Int64), P x)

theorem Int64.exists_iff_exists_ofBitVec {P : Int64 → Prop} : (∃ (x : Int64), P x) ↔ ∃ (x : BitVec 64), P (ofBitVec x)

theorem Int64.forall_iff_forall_ofBitVec {P : Int64 → Prop} : (∀ (x : Int64), P x) ↔ ∀ (x : BitVec 64), P (ofBitVec x)

@[instance_reducible]

instance Int64.instDecidableForall (P : Int64 → Prop) [DecidablePred P] : Decidable (∀ (x : Int64), P x)