mathlib documentation

core / init.data.list.instances

@[protected, instance]
Equations
@[protected, instance]
@[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
@[protected, instance]
def list.decidable_ball {α : Type u} (p : α → Prop) [decidable_pred p] (l : list α) :
decidable (∀ (x : α), x lp x)
Equations