mathlib documentation

core / init.data.list.instances

@[instance]
Equations
@[instance]
def list.bin_tree_to_list {α : Type u} :
Equations
@[instance]
def list.decidable_bex {α : Type u} (p : α → Prop) [decidable_pred p] (l : list α) :
decidable (∃ (x : α) (H : x l), p x)
Equations
@[instance]
def list.decidable_ball {α : Type u} (p : α → Prop) [decidable_pred p] (l : list α) :
decidable (∀ (x : α), x lp x)
Equations