Skip to content

feat: adding free reader monad API and minor edits to free writer and free cont#247

Merged
fmontesi merged 8 commits intoleanprover:mainfrom
tannerduve:tannerduve/free-monad-edits
Jan 15, 2026
Merged

feat: adding free reader monad API and minor edits to free writer and free cont#247
fmontesi merged 8 commits intoleanprover:mainfrom
tannerduve:tannerduve/free-monad-edits

Conversation

@tannerduve
Copy link
Contributor

This PR adds an API for the Reader monad represented as a free monad, to the list of existing free effects. Also made some minor changes to the Writer and Cont APIs in this same file

@tannerduve tannerduve force-pushed the tannerduve/free-monad-edits branch from 59483c2 to 235d946 Compare January 7, 2026 23:08
@chenson2018
Copy link
Collaborator

@eric-wieser @quangvdao I recall you having thoughts on the initial PR, anything for this one?

@quangvdao
Copy link

none, looks good to me. glad this is now in cslib!

@tannerduve
Copy link
Contributor Author

tannerduve commented Jan 13, 2026

@eric-wieser i added censor because it is in the writer monad API in haskell, but it is probably not needed here since its not in the lean API

Since this PR is meant to be about adding the reader monad to the free effects library, I think I'll just remove the censor stuff for now

@fmontesi fmontesi added this pull request to the merge queue Jan 15, 2026
Merged via the queue into leanprover:main with commit 26c0474 Jan 15, 2026
2 checks passed
@tannerduve tannerduve deleted the tannerduve/free-monad-edits branch January 15, 2026 21:44
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

5 participants