Skip to content
This repository was archived by the owner on Jul 24, 2024. It is now read-only.

[Merged by Bors] - feat(*): bump to lean 3.48.0#16292

Closed
gebner wants to merge 3 commits intomasterfrom
finstruct
Closed

[Merged by Bors] - feat(*): bump to lean 3.48.0#16292
gebner wants to merge 3 commits intomasterfrom
finstruct

Conversation

@gebner
Copy link
Copy Markdown
Member

@gebner gebner commented Aug 29, 2022 •
edited by github-actions bot
Loading

@gebner gebner added WIP Work in progress mathport For compatibility with Lean 4 changes, to simplify porting labels Aug 29, 2022
@ghost ghost added the blocked-by-other-PR This PR depends on another PR which is still in the queue. A bot manages this label via PR comment. label Aug 29, 2022
@gebner gebner added awaiting-review The author would like community review of the PR merge-conflict Please `git merge origin/master` then a bot will remove this label. and removed WIP Work in progress labels Aug 30, 2022
@ghost ghost removed the blocked-by-other-PR This PR depends on another PR which is still in the queue. A bot manages this label via PR comment. label Aug 31, 2022
@ghost
Copy link
Copy Markdown

ghost commented Aug 31, 2022

This PR/issue depends on:

@gebner gebner removed the merge-conflict Please `git merge origin/master` then a bot will remove this label. label Aug 31, 2022
jcommelin
jcommelin approved these changes Aug 31, 2022
View reviewed changes
Copy link
Copy Markdown
Member

@jcommelin jcommelin left a comment

Choose a reason for hiding this comment

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

Thanks 🎉

bors merge

@leanprover-community-bot-assistant leanprover-community-bot-assistant added ready-to-merge All that is left is for bors to build and merge this PR. (Remember you need to say `bors r+`.) and removed awaiting-review The author would like community review of the PR labels Aug 31, 2022
bors bot pushed a commit that referenced this pull request Aug 31, 2022
@gebner
feat(*): bump to lean 3.48.0 (#16292)
acbe099 
`fin n` is a structure now.
@bors
Copy link
Copy Markdown

bors bot commented Aug 31, 2022

Pull request successfully merged into master.

Build succeeded:

@bors bors bot changed the title feat(*): bump to lean 3.48.0 [Merged by Bors] - feat(*): bump to lean 3.48.0 Aug 31, 2022
@bors bors bot closed this Aug 31, 2022
@bors bors bot deleted the finstruct branch August 31, 2022 23:05
Sign up for free to subscribe to this conversation on GitHub. Already have an account? Sign in.

Reviewers

1 more reviewer

@jcommelin jcommelin jcommelin approved these changes

Reviewers whose approvals may not affect merge requirements

Assignees

No one assigned

Labels

mathport For compatibility with Lean 4 changes, to simplify porting ready-to-merge All that is left is for bors to build and merge this PR. (Remember you need to say `bors r+`.)

Projects

None yet

Milestone

No milestone

Development

Successfully merging this pull request may close these issues.

3 participants

@gebner @jcommelin @leanprover-community-bot-assistant