Skip to content

RFunctor of Agree - #118

Merged
markusdemedeiros merged 4 commits into
leanprover-community:masterfrom
screenl:agreefunctor
Jan 22, 2026
Merged

markusdemedeiros merged 4 commits into
leanprover-community:masterfrom
screenl:agreefunctor

Conversation

@screenl

@screenl screenl commented Jan 18, 2026

Copy link
Copy Markdown
Contributor

closes #30

@markusdemedeiros

Copy link
Copy Markdown
Collaborator

Thanks, and great to see you here! I did a little bit of golfing, but overall his looks great.

If you're in the mood to port more, there are lots of other OFunctors that are immediately accessible!

@markusdemedeiros
markusdemedeiros merged commit 6ec77ab into leanprover-community:master Jan 22, 2026
1 check passed
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Projects

None yet

Development

Successfully merging this pull request may close these issues.

Agreement OFunctors

3 participants