Skip to content

feat: correctness for Fin.foldl and Fin.foldr#528

Merged
digama0 merged 6 commits intoleanprover-community:mainfrom
fgdorais:finfold
Mar 21, 2024
Merged

feat: correctness for Fin.foldl and Fin.foldr#528
digama0 merged 6 commits intoleanprover-community:mainfrom
fgdorais:finfold

Conversation

@fgdorais
Copy link
Copy Markdown
Collaborator

No description provided.

@fgdorais fgdorais added the awaiting-review This PR is ready for review; the author thinks it is ready to be merged. label Jan 15, 2024
Copy link
Copy Markdown
Collaborator

@kim-em kim-em left a comment

Choose a reason for hiding this comment

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

LGTM

@ghost ghost added the merge-conflict This PR has merge conflicts with the `main` branch which must be resolved by the author. label Jan 17, 2024
@ghost ghost added merge-conflict This PR has merge conflicts with the `main` branch which must be resolved by the author. and removed merge-conflict This PR has merge conflicts with the `main` branch which must be resolved by the author. labels Jan 29, 2024
@ghost ghost removed the merge-conflict This PR has merge conflicts with the `main` branch which must be resolved by the author. label Feb 18, 2024
@fgdorais fgdorais force-pushed the finfold branch 3 times, most recently from 9a41785 to f291f49 Compare February 18, 2024 03:04
@fgdorais
Copy link
Copy Markdown
Collaborator Author

Some weird git issues happened here. On hold for now.

@fgdorais
Copy link
Copy Markdown
Collaborator Author

Git issues fixed but history may have been mangled a bit during surgery. Let's merge this soon before it rots again.

@ghost ghost added the merge-conflict This PR has merge conflicts with the `main` branch which must be resolved by the author. label Mar 5, 2024
@ghost ghost removed the merge-conflict This PR has merge conflicts with the `main` branch which must be resolved by the author. label Mar 18, 2024
@digama0 digama0 merged commit 6267b3e into leanprover-community:main Mar 21, 2024
@fgdorais fgdorais mentioned this pull request Jul 30, 2024
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

awaiting-review This PR is ready for review; the author thinks it is ready to be merged.

Projects

None yet

Development

Successfully merging this pull request may close these issues.

5 participants