core / init.data.list.instances

@[protected, instance]

def list.monad :

Equations

@[protected, instance]

@[protected, instance]

def list.alternative :

Equations

@[protected, instance]

def list.bin_tree_to_list {α : Type u} :

Equations

@[protected, instance]

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

decidable (∃ (x : α) (H : x ∈ l), p x)

Equations

list.decidable_bex p (x :: xs) = dite (p x) (λ (h₁ : p x), decidable.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 = decidable.is_false _
list.decidable_bex._match_1 p x xs h₁ (decidable.is_true h₂) = decidable.is_true _
list.decidable_bex._match_1 p x xs h₁ (decidable.is_false h₂) = decidable.is_false _

@[protected, 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), decidable.is_false _) (λ (h : ¬∃ (x : α) (H : x ∈ l), ¬p x), decidable.is_true _)
_ = _