Init.Data.List.Control

source

@[specialize]

def List.mapM {m : Type u → Type v} [inst : Monad m] {α : Type w} {β : Type u} (f : α → m β) :

List α → m (List β)

Equations

List.mapM f [] = pure []
List.mapM f (a :: as) = do let a ← f a let a_1 ← List.mapM f as pure (a :: a_1)

source

@[specialize]

def List.mapA {m : Type u → Type v} [inst : Applicative m] {α : Type w} {β : Type u} (f : α → m β) :

List α → m (List β)

Equations

List.mapA f [] = pure []
List.mapA f (a :: as) = Seq.seq (List.cons <$> f a) fun x => List.mapA f as

source

@[specialize]

def List.forM {m : Type u → Type v} [inst : Monad m] {α : Type w} (as : List α) (f : α → m PUnit) :

m PUnit

Equations

List.forM [] f = pure PUnit.unit
List.forM (a :: as_1) f = do f a List.forM as_1 f

source

@[specialize]

def List.forA {m : Type u → Type v} [inst : Applicative m] {α : Type w} (as : List α) (f : α → m PUnit) :

m PUnit

Equations

List.forA [] f = pure PUnit.unit
List.forA (a :: as_1) f = SeqRight.seqRight (f a) fun x => List.forA as_1 f

source

@[specialize]

def List.filterAuxM {m : Type → Type v} [inst : Monad m] {α : Type} (f : α → m Bool) :

List α → List α → m (List α)

Equations

List.filterAuxM f [] _fun_discr = pure _fun_discr
List.filterAuxM f (h :: t) _fun_discr = do let b ← f h List.filterAuxM f t (cond b (h :: _fun_discr) _fun_discr)

source

@[inline]

def List.filterM {m : Type → Type v} [inst : Monad m] {α : Type} (f : α → m Bool) (as : List α) :

m (List α)

Equations

List.filterM f as = do let as ← List.filterAuxM f as [] pure (List.reverse as)

source

@[inline]

def List.filterRevM {m : Type → Type v} [inst : Monad m] {α : Type} (f : α → m Bool) (as : List α) :

m (List α)

Equations

List.filterRevM f as = List.filterAuxM f (List.reverse as) []

source

@[inline]

def List.filterMapM {m : Type u → Type v} [inst : Monad m] {α : Type u} {β : Type u} (f : α → m (Option β)) (as : List α) :

m (List β)

Equations

List.filterMapM f as = List.filterMapM.loop f (List.reverse as) []

source

@[specialize]

def List.filterMapM.loop {m : Type u → Type v} [inst : Monad m] {α : Type u} {β : Type u} (f : α → m (Option β)) :

List α → List β → m (List β)

Equations

List.filterMapM.loop f [] _fun_discr = pure _fun_discr
List.filterMapM.loop f (a :: as) _fun_discr = do let a ← f a match a with | none => List.filterMapM.loop f as _fun_discr | some b => List.filterMapM.loop f as (b :: _fun_discr)

source

@[specialize]

def List.foldlM {m : Type u → Type v} [inst : Monad m] {s : Type u} {α : Type w} (f : s → α → m s) (init : s) :

List α → m s

Equations

List.foldlM _fun_discr _fun_discr [] = pure _fun_discr
List.foldlM _fun_discr _fun_discr (a :: as) = do let s' ← _fun_discr _fun_discr a List.foldlM _fun_discr s' as

source

@[specialize]

def List.foldrM {m : Type u → Type v} [inst : Monad m] {s : Type u} {α : Type w} (f : α → s → m s) (init : s) :

List α → m s

Equations

List.foldrM _fun_discr _fun_discr [] = pure _fun_discr
List.foldrM _fun_discr _fun_discr (a :: as) = do let s' ← List.foldrM _fun_discr _fun_discr as _fun_discr a s'

source

@[specialize]

def List.firstM {m : Type u → Type v} [inst : Monad m] [inst : Alternative m] {α : Type w} {β : Type u} (f : α → m β) :

List α → m β

Equations

List.firstM f [] = failure
List.firstM f (a :: as) = HOrElse.hOrElse (f a) fun x => List.firstM f as

source

@[specialize]

def List.anyM {m : Type → Type u} [inst : Monad m] {α : Type v} (f : α → m Bool) :

List α → m Bool

Equations

List.anyM f [] = pure false
List.anyM f (a :: as) = do let a ← f a match a with | true => pure true | false => List.anyM f as

source

@[specialize]

def List.allM {m : Type → Type u} [inst : Monad m] {α : Type v} (f : α → m Bool) :

List α → m Bool

Equations

List.allM f [] = pure true
List.allM f (a :: as) = do let a ← f a match a with | true => List.allM f as | false => pure false

source

@[specialize]

def List.findM? {m : Type → Type u} [inst : Monad m] {α : Type} (p : α → m Bool) :

List α → m (Option α)

Equations

List.findM? p [] = pure none
List.findM? p (a :: as) = do let a ← p a match a with | true => pure (some a) | false => List.findM? p as

source

@[specialize]

def List.findSomeM? {m : Type u → Type v} [inst : Monad m] {α : Type w} {β : Type u} (f : α → m (Option β)) :

List α → m (Option β)

Equations

List.findSomeM? f [] = pure none
List.findSomeM? f (a :: as) = do let a ← f a match a with | some b => pure (some b) | none => List.findSomeM? f as

source

@[inline]

def List.forIn {α : Type u} {β : Type v} {m : Type v → Type w} [inst : Monad m] (as : List α) (init : β) (f : α → β → m (ForInStep β)) :

m β

Equations

List.forIn as init f = List.forIn.loop f as init

source

@[specialize]

def List.forIn.loop {α : Type u} {β : Type v} {m : Type v → Type w} [inst : Monad m] (f : α → β → m (ForInStep β)) :

List α → β → m β

Equations

List.forIn.loop f [] _fun_discr = pure _fun_discr
List.forIn.loop f (a :: as) _fun_discr = do let a ← f a _fun_discr match a with | ForInStep.done b => pure b | ForInStep.yield b => List.forIn.loop f as b

source

instance List.instForInList {m : Type u_1 → Type u_2} {α : Type u_3} :

ForIn m (List α) α

Equations

List.instForInList = { forIn := fun {β} [Monad m] => List.forIn }

source

@[simp]

theorem List.forIn_nil {m : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_1} [inst : Monad m] (f : α → β → m (ForInStep β)) (b : β) :

forIn [] b f = pure b

source

@[simp]

theorem List.forIn_cons {m : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_1} [inst : Monad m] (f : α → β → m (ForInStep β)) (a : α) (as : List α) (b : β) :

forIn (a :: as) b f = do let _fun_discr ← f a b match _fun_discr with | ForInStep.done b => pure b | ForInStep.yield b => forIn as b f

source

@[inline]

def List.forIn' {α : Type u} {β : Type v} {m : Type v → Type w} [inst : Monad m] (as : List α) (init : β) (f : (a : α) → a ∈ as → β → m (ForInStep β)) :

m β

Equations

List.forIn' as init f = List.forIn'.loop as f as init (_ : ∃ bs, bs ++ as = as)

source

@[specialize]

def List.forIn'.loop {α : Type u} {β : Type v} {m : Type v → Type w} [inst : Monad m] (as : List α) (f : (a : α) → a ∈ as → β → m (ForInStep β)) :

(_fun_discr : List α) → β → (∃ bs, bs ++ _fun_discr = as) → m β

source

instance List.instForIn'ListInferInstanceMembershipInstMembershipList {m : Type u_1 → Type u_2} {α : Type u_3} :

ForIn' m (List α) α inferInstance

Equations

List.instForIn'ListInferInstanceMembershipInstMembershipList = { forIn' := fun {β} [Monad m] => List.forIn' }

source

@[simp]

theorem List.forIn'_eq_forIn {α : Type u} {β : Type v} {m : Type v → Type w} [inst : Monad m] (as : List α) (init : β) (f : α → β → m (ForInStep β)) :

(forIn' as init fun a x b => f a b) = forIn as init f

source

instance List.instForMList {m : Type u_1 → Type u_2} {α : Type u_3} :

ForM m (List α) α

Equations

List.instForMList = { forM := fun [Monad m] => List.forM }

source

@[simp]

theorem List.forM_nil {m : Type u_1 → Type u_2} {α : Type u_3} [inst : Monad m] (f : α → m PUnit) :

forM [] f = pure PUnit.unit

source

@[simp]

theorem List.forM_cons {m : Type u_1 → Type u_2} {α : Type u_3} [inst : Monad m] (f : α → m PUnit) (a : α) (as : List α) :

forM (a :: as) f = do f a forM as f