Structures · Lean core

Monad

[Monads](https://en.wikipedia.org/wiki/Monad_(functional_programming)) are an abstraction of sequential control flow and side effects used in functional programming. Monads allow both sequencing of effects and data-dependent effects: the values that result from an early step may influence the effects carried out in a later step. The Monad API may be used directly. However, it is most commonly accessed through [do-notation](https://lean-lang.org/doc/reference/4.33.0/find/?domain=Verso.Genre.Manual.section&name=do-notation). Most Monad instances provide implementations of pure and bind, and use default implementations for the other methods inherited from Applicative. Monads should satisfy certain laws, but instances are not required to prove this. An instance of LawfulMonad expresses that a given monad's operations are lawful.

Defined in

Init.Prelude

Shape

One type argument