mathlib documentation

core / init.data.list.instances

source
@[protected, instance]
def list.monad  :
monad list
Equations
source
@[protected, instance]
def list.is_lawful_monad  :
is_lawful_monad list
source
@[protected, instance]
def list.alternative  :
alternative list
Equations
source
@[protected, instance]
def list.bin_tree_to_list {α : Type u} :
has_coe (bin_tree α) (list α)
Equations
source
@[protected, instance]
def list.decidable_bex {α : Type u} (p : α → Prop) [decidable_pred p] (l : list α) :
decidable (∃ (x : α) (H : x ∈ l), p x)
Equations
source
@[protected, instance]
def list.decidable_ball {α : Type u} (p : α → Prop) [decidable_pred p] (l : list α) :
decidable (∀ (x : α), x ∈ l → p x)
Equations