Decidable Instances for List not (yet) in Std

theorem List.bind_singleton {α : Type u} {β : Type v} (f : α → List β) (x : α) : List.bind [x] f = f x

@[simp]

theorem List.bind_singleton' {α : Type u} (l : List α) : (List.bind l fun x => [x]) = l

theorem List.map_eq_bind {α : Type u_1} {β : Type u_2} (f : α → β) (l : List α) : List.map f l = List.bind l fun x => [f x]

theorem List.bind_assoc {γ : Type w} {α : Type u_1} {β : Type u_2} (l : List α) (f : α → List β) (g : β → List γ) : List.bind (List.bind l f) g = List.bind l fun x => List.bind (f x) g

instance List.instMonad : Monad List

Equations

• List.instMonad = Monad.mk

instance List.instLawfulMonad : LawfulMonad List

Equations

• List.instLawfulMonad = List.instLawfulMonad.proof_1

instance List.instAlternative : Alternative List

Equations

• List.instAlternative = Alternative.mk @List.nil fun {α} l l' => List.append l (l' ())

instance List.decidableBex {α : Type u} {p : α → Prop} [DecidablePred p] (l : List α) : Decidable (∃ x, x ∈ l ∧ p x)

Equations

• One or more equations did not get rendered due to their size.
• List.decidableBex [] = isFalse (_ : ¬∃ x, x ∈ [] ∧ p x)

instance List.decidableBall {α : Type u} {p : α → Prop} [DecidablePred p] (l : List α) : Decidable ((x : α) → x ∈ l → p x)

Equations

• List.decidableBall l = match inferInstance with | isFalse h => isTrue (List.decidableBall.proof_1 l h) | isTrue h => isFalse (_ : ¬((x : α) → x ∈ l → p x))