Documentation

Mathlib.Init.Data.List.Instances

Decidable Instances for List not (yet) in Std

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