Theorems · Definition

Traversable.traverse

{t : Type u → Type u} →
  [self : Traversable t] → {m : Type u → Type u} → [Applicative m] → {α β : Type u} → (α → m β) → t α → m (t β)

The function commuting a traversable functor t with an arbitrary applicative functor m.

Defined in

Mathlib.Control.Traversable.Basic

Cited by

53 results in Mathlib

Foundations

Depth 1 from the axioms · uses no axioms

Assumes

TraversableApplicative