mathlib3 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 l p x)
Equations