def Array.decideBoolArray (p : Array Bool → Bool) (n : ℕ) : Bool

Equations

• Array.decideBoolArray p n = List.decideBoolList (fun (x : List Bool) => p { toList := x }) n

theorem Array.decideBoolArray_iff {p : Array Bool → Prop} [hp : DecidablePred p] {n : ℕ} : decideBoolArray (fun (b : Array Bool) => decide (p b)) n = true ↔ ∀ (xs : Array Bool), xs.size = n → p xs

@[instance_reducible]

instance Array.instDecidableForallForallEqNatSizeBoolOfDecidablePred_projects {p : Array Bool → Prop} [hp : DecidablePred p] {n : ℕ} : Decidable (∀ (xs : Array Bool), xs.size = n → p xs)

Equations

• Array.instDecidableForallForallEqNatSizeBoolOfDecidablePred_projects = decidable_of_bool (Array.decideBoolArray (fun (b : Array Bool) => decide (p b)) n) ⋯