Decidable Instances for List not (yet) in Std

ink

instance List.decidableBex {α : Type u_1} {p : α → Prop} [inst : 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)

ink

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

Equations

• List.decidableBall l = if h : ∃ x, x ∈ l ∧ ¬p x then isFalse (_ : ¬((x : α) → x ∈ l → p x)) else isTrue (List.decidableBall.proof_2 l h)