Mathlib Map

Structures · Lean core

AlternativeMonad

AlternativeMonad m means that m has both a Monad and Alternative instance, which both share the same underlying Applicative instance. The main example is Option, but many monad transformers also preserve or add this structure.

Defined in
Batteries.Control.AlternativeMonad
Shape
One type argument

Extends2

Extended by0

Nothing extends this class yet.

Concrete types that are instances11

  • ReaderT
  • StateT
  • StateRefT'
  • OptionT
  • Lean.Meta.MetaM
  • MLList
  • SetM
  • Nondet
  • List
  • Finset
  • Option

How is a type an instance?

Loading the hierarchy index…

Assumed by2

Ancestors15