Mathlib Map

Structures · Lean core

LawfulMonad

Lawful monads are those that satisfy a certain behavioral specification. While all instances of Monad should satisfy these laws, not all implementations are required to prove this. LawfulMonad.mk' is an alternative constructor that contains useful defaults for many fields.

Defined in
Init.Control.Lawful.Basic
Shape
One type argument · adds bind_pure_comp, bind_map, pure_bind, bind_assoc
Open in Mathlib docs

Extends1

Extended by4

Concrete types that are instances53

  • FreeAbelianGroup
  • FreeGroup
  • FreeAddGroup
  • MvPolynomial
  • Part
  • ReaderT
  • StateT
  • Except
  • StateRefT'
  • OptionT
  • Ultrafilter
  • Lean.Core.CoreM
  • ExceptT
  • Lean.Elab.Command.CommandElabM
  • Semiquot
  • PFun
  • FreeMagma
  • EStateM
  • FreeSemigroup
  • EIO
  • Lean.Elab.Term.TermElabM
  • FreeAddMagma
  • Lean.Meta.MetaM
  • FreeAddSemigroup
  • ST
  • Computation
  • EST
  • BaseIO
  • Stream'.Seq1
  • Std.Internal.Do.PredTrans
  • SetM
  • Std.Iterators.PostconditionT
  • Erased
  • Lean.Elab.Tactic.TacticM
  • Std.Do.PredTrans
  • ContT
  • WriterT
  • Std.Iterators.HetT
  • PMF
  • ExceptCpsT
  • StateCpsT
  • Std.Iterators.ULiftT
  • IO
  • ULift
  • Sum
  • List
  • Set
  • Multiset
  • Finset
  • Option
  • PLift
  • Id
  • Trunc

How is a type an instance?

Loading the hierarchy index…

Assumed by42

Ancestors2