instLawfulMonad — Mathlib

English

The List type constructor forms a LawfulMonad with the usual map, pure, and bind operations.

Русский

Тип List образует LawfulMonad с обычными операциями map, pure и bind.

LaTeX

$$$\\mathrm{LawfulMonad}(\\mathrm List)$$

Lean4

instance instLawfulMonad : LawfulMonad List.{u} :=
  LawfulMonad.mk' (id_map := map_id) (pure_bind := fun _ _ => List.append_nil _) (bind_assoc := fun _ _ _ =>
    List.flatMap_assoc) (bind_pure_comp := fun _ _ => map_eq_flatMap.symm)

Похожие утверждения