def commandDeclare_decidable_uint_quantifiers__ : Lean.ParserDescr

Equations

• One or more equations did not get rendered due to their size.

@[instance_reducible]

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

Equations

• UInt8.instDecidableExists P = decidable_of_iff' (∃ (x : BitVec 8), P { toBitVec := x }) ⋯

theorem UInt8.forall_iff_forall_ofBitVec {P : UInt8 → Prop} : (∀ (x : UInt8), P x) ↔ ∀ (x : BitVec 8), P { toBitVec := x }

@[instance_reducible]

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

Equations

• UInt8.instDecidableForall P = decidable_of_iff' (∀ (x : BitVec 8), P { toBitVec := x }) ⋯

theorem UInt8.exists_iff_exists_ofBitVec {P : UInt8 → Prop} : (∃ (x : UInt8), P x) ↔ ∃ (x : BitVec 8), P { toBitVec := x }

@[instance_reducible]

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

Equations

• UInt16.instDecidableForall P = decidable_of_iff' (∀ (x : BitVec 16), P { toBitVec := x }) ⋯

theorem UInt16.exists_iff_exists_ofBitVec {P : UInt16 → Prop} : (∃ (x : UInt16), P x) ↔ ∃ (x : BitVec 16), P { toBitVec := x }

theorem UInt16.forall_iff_forall_ofBitVec {P : UInt16 → Prop} : (∀ (x : UInt16), P x) ↔ ∀ (x : BitVec 16), P { toBitVec := x }

@[instance_reducible]

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

Equations

• UInt16.instDecidableExists P = decidable_of_iff' (∃ (x : BitVec 16), P { toBitVec := x }) ⋯

theorem UInt32.exists_iff_exists_ofBitVec {P : UInt32 → Prop} : (∃ (x : UInt32), P x) ↔ ∃ (x : BitVec 32), P { toBitVec := x }

@[instance_reducible]

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

Equations

• UInt32.instDecidableExists P = decidable_of_iff' (∃ (x : BitVec 32), P { toBitVec := x }) ⋯

@[instance_reducible]

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

Equations

• UInt32.instDecidableForall P = decidable_of_iff' (∀ (x : BitVec 32), P { toBitVec := x }) ⋯

theorem UInt32.forall_iff_forall_ofBitVec {P : UInt32 → Prop} : (∀ (x : UInt32), P x) ↔ ∀ (x : BitVec 32), P { toBitVec := x }

@[instance_reducible]

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

Equations

• UInt64.instDecidableExists P = decidable_of_iff' (∃ (x : BitVec 64), P { toBitVec := x }) ⋯

theorem UInt64.forall_iff_forall_ofBitVec {P : UInt64 → Prop} : (∀ (x : UInt64), P x) ↔ ∀ (x : BitVec 64), P { toBitVec := x }

@[instance_reducible]

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

Equations

• UInt64.instDecidableForall P = decidable_of_iff' (∀ (x : BitVec 64), P { toBitVec := x }) ⋯

theorem UInt64.exists_iff_exists_ofBitVec {P : UInt64 → Prop} : (∃ (x : UInt64), P x) ↔ ∃ (x : BitVec 64), P { toBitVec := x }