English
The partial type Part forms a lawful monad, satisfying the standard monad laws (bind, map, pure, and associativity).
Русский
Тип Part образует законный монад, удовлетворяющий стандартным законам монад (bind, map, pure и ассоциативность).
LaTeX
$$$\text{LawfulMonad}(\text{Part})$$$
Lean4
instance : LawfulMonad Part where
bind_pure_comp := @bind_some_eq_map
id_map f := by cases f; rfl
pure_bind := @bind_some
bind_assoc := @bind_assoc
map_const := by
simp [Functor.mapConst, Functor.map]
--Porting TODO : In Lean3 these were automatic by a tactic
seqLeft_eq x
y := ext' (by simp [SeqLeft.seqLeft, Part.bind, assert, Seq.seq, const, (· <$> ·), and_comm]) (fun _ _ => rfl)
seqRight_eq x y := ext' (by simp [SeqRight.seqRight, Part.bind, assert, Seq.seq, const, (· <$> ·)]) (fun _ _ => rfl)
pure_seq x y := ext' (by simp [Seq.seq, Part.bind, assert, (· <$> ·), pure]) (fun _ _ => rfl)
bind_map x y := ext' (by simp [(· >>= ·), Part.bind, assert, Seq.seq, (· <$> ·)]) (fun _ _ => rfl)
