instLawfulMonad — Mathlib

English

The Erased type forms a Lawful Monad; all Monad, Functor, and Applicative laws hold coherently for Erased.

Русский

Тип Erased образует законный монад; все законы монад, функторa и аппликативности выполняются согласованно.

LaTeX

$$$\\text{LawfulMonad}(\\mathrm{Erased})$$$

Lean4

protected instance instLawfulMonad : LawfulMonad Erased :=
  { id_map := by intros; ext; simp
    map_const := by intros; ext; simp [Functor.mapConst]
    pure_bind := by intros; ext; simp
    bind_assoc := by intros; ext; simp
    bind_pure_comp := by intros; ext; simp
    bind_map := by intros; ext; simp [Seq.seq]
    seqLeft_eq := by intros; ext; simp [Seq.seq, SeqLeft.seqLeft]
    seqRight_eq := by intros; ext; simp [Seq.seq, SeqRight.seqRight]
    pure_seq := by intros; ext; simp [Seq.seq] }

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