mathlib docs: core.init.data.list.instances

list.decidable_bex p (x :: xs) = dite (p x) (λ (h₁ : p x), is_true _) (λ (h₁ : ¬p x), list.decidable_bex._match_1 p x xs h₁ (list.decidable_bex p xs))
list.decidable_bex p list.nil = is_false _
list.decidable_bex._match_1 p x xs h₁ (is_true h₂) = is_true _
list.decidable_bex._match_1 p x xs h₁ (is_false h₂) = is_false _

@[instance]

def list.decidable_ball {α : Type u} (p : α → Prop) [decidable_pred p] (l : list α) :

decidable (∀ (x : α), x ∈ l → p x)

Equations

list.decidable_ball p l = dite (∃ (x : α) (H : x ∈ l), ¬p x) (λ (h : ∃ (x : α) (H : x ∈ l), ¬p x), is_false _) (λ (h : ¬∃ (x : α) (H : x ∈ l), ¬p x), is_true _)
_ = _