Init.Data.UInt.Decidable

Instances For

source

@[instance_reducible]

instance UInt8.instDecidableExists (P : UInt8 → Prop) [DecidablePred P] :

Decidable (∃ (x : UInt8 ), P x)

source

theorem UInt8.forall_iff_forall_ofBitVec {P : UInt8 → Prop} :

(∀ (x : UInt8), P x) ↔ ∀ (x : BitVec 8), P { toBitVec := x }

source

@[instance_reducible]

instance UInt8.instDecidableForall (P : UInt8 → Prop) [DecidablePred P] :

Decidable (∀ (x : UInt8), P x)

source

theorem UInt8.exists_iff_exists_ofBitVec {P : UInt8 → Prop} :

(∃ (x : UInt8 ), P x) ↔ ∃ (x : BitVec 8), P { toBitVec := x }

source

@[instance_reducible]

instance UInt16.instDecidableForall (P : UInt16 → Prop) [DecidablePred P] :

Decidable (∀ (x : UInt16), P x)

source

theorem UInt16.exists_iff_exists_ofBitVec {P : UInt16 → Prop} :

(∃ (x : UInt16 ), P x) ↔ ∃ (x : BitVec 16), P { toBitVec := x }

source

theorem UInt16.forall_iff_forall_ofBitVec {P : UInt16 → Prop} :

(∀ (x : UInt16), P x) ↔ ∀ (x : BitVec 16), P { toBitVec := x }

source

@[instance_reducible]

instance UInt16.instDecidableExists (P : UInt16 → Prop) [DecidablePred P] :

Decidable (∃ (x : UInt16 ), P x)

source

theorem UInt32.exists_iff_exists_ofBitVec {P : UInt32 → Prop} :

(∃ (x : UInt32 ), P x) ↔ ∃ (x : BitVec 32), P { toBitVec := x }

source

@[instance_reducible]

instance UInt32.instDecidableExists (P : UInt32 → Prop) [DecidablePred P] :

Decidable (∃ (x : UInt32 ), P x)

source

@[instance_reducible]

instance UInt32.instDecidableForall (P : UInt32 → Prop) [DecidablePred P] :

Decidable (∀ (x : UInt32), P x)

source

theorem UInt32.forall_iff_forall_ofBitVec {P : UInt32 → Prop} :

(∀ (x : UInt32), P x) ↔ ∀ (x : BitVec 32), P { toBitVec := x }

source

@[instance_reducible]

instance UInt64.instDecidableExists (P : UInt64 → Prop) [DecidablePred P] :

Decidable (∃ (x : UInt64 ), P x)

source

theorem UInt64.forall_iff_forall_ofBitVec {P : UInt64 → Prop} :

(∀ (x : UInt64), P x) ↔ ∀ (x : BitVec 64), P { toBitVec := x }

source

@[instance_reducible]

instance UInt64.instDecidableForall (P : UInt64 → Prop) [DecidablePred P] :

Decidable (∀ (x : UInt64), P x)

source

theorem UInt64.exists_iff_exists_ofBitVec {P : UInt64 → Prop} :

(∃ (x : UInt64 ), P x) ↔ ∃ (x : BitVec 64), P { toBitVec := x }