Skip to content

refactor: change the simpNF for FreeM#417

Open
eric-wieser wants to merge 5 commits intomainfrom
eric-wieser/freeM-simpNF
Open

refactor: change the simpNF for FreeM#417
eric-wieser wants to merge 5 commits intomainfrom
eric-wieser/freeM-simpNF

Conversation

@eric-wieser
Copy link
Copy Markdown
Collaborator

@eric-wieser eric-wieser commented Mar 11, 2026 •
edited
Loading

This declares liftBind an implementation detail, encouraging users to work with lift and bind separately instead.

Depends on:
eric-wieser
eric-wieser commented Mar 11, 2026
View reviewed changes
Cslib/Foundations/Control/Monad/Free/Effects.lean
Comment on lines +227 to +243
-- https://github.com/leanprover-community/mathlib4/pull/36497
section missing_from_mathlib

@[simp]
theorem _root_.WriterT.run_pure [Monoid ω] [Monad M] (a : α) :
WriterT.run (pure a : WriterT ω M α) = pure (a, 1) := rfl

@[simp]
theorem _root_.WriterT.run_bind [Monoid ω] [Monad M] (x : WriterT ω M α) (f : α → WriterT ω M β) :
WriterT.run (x >>= f) = x.run >>= fun (a, w₁) => (fun (b, w₂) => (b, w₁ * w₂)) <$> (f a).run :=
rfl

@[simp]
theorem _root_.WriterT.run_tell [Monad M] (w : ω) :
WriterT.run (MonadWriter.tell w : WriterT ω M PUnit) = pure (.unit, w) := rfl

end missing_from_mathlib
Copy link
Copy Markdown
Collaborator Author

@eric-wieser eric-wieser Mar 11, 2026

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

leanprover-community/mathlib4#36497
@eric-wieser eric-wieser force-pushed the eric-wieser/freeM-simpNF branch from 666ea00 to e6ed134 Compare March 11, 2026 23:01
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

1 participant

@eric-wieser