Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

[Merged by Bors] - chore(*): update to Lean 3.21.0c #4578

Closed
wants to merge 16 commits into from
Closed

[Merged by Bors] - chore(*): update to Lean 3.21.0c #4578

wants to merge 16 commits into from

Conversation

bryangingechen
Copy link
Collaborator

@bryangingechen bryangingechen commented Oct 12, 2020 •
edited
Loading

The only real change is the removal of notation for vector.cons.

@bryangingechen bryangingechen added the WIP Work in progress label Oct 12, 2020
@bryangingechen
Copy link
Collaborator Author

@digama0 suggested adding back a notation for vector.cons in data.vector2.

Anyone reading this should feel free to take this on, otherwise I'll do this later.

@jcommelin jcommelin added awaiting-review The author would like community review of the PR and removed WIP Work in progress labels Oct 12, 2020
@bryangingechen bryangingechen mentioned this pull request Oct 12, 2020
Closed
5 tasks
@robertylewis
Copy link
Member

bors merge

@github-actions github-actions bot 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 Oct 12, 2020
@bryangingechen bryangingechen mentioned this pull request Oct 12, 2020
Closed
1 task
bors bot pushed a commit that referenced this pull request Oct 12, 2020
@bryangingechen @jcommelin
chore(*): update to Lean 3.21.0c (#4578)
9713e96 
The only real change is the removal of notation for `vector.cons`.



Co-authored-by: Johan Commelin <johan@commelin.net>
@bors
Copy link

bors bot commented Oct 12, 2020

Pull request successfully merged into master.

Build succeeded:

@bors bors bot changed the title chore(*): update to Lean 3.21.0c [Merged by Bors] - chore(*): update to Lean 3.21.0c Oct 12, 2020
@bors bors bot closed this Oct 12, 2020
@bors bors bot deleted the bryangingechen-patch-1 branch October 12, 2020 20:49
@bryangingechen
Copy link
Collaborator Author

Hmm, it's too late now, but I should have mentioned the new notation in the commit message.

bors bot pushed a commit that referenced this pull request Oct 13, 2020
@pechersky @urkud @bryangingechen
feat(data/vector2): induction principle, define last, and some lemmas…
7cff825 
… (blocked by #4578) (#4554)

Co-authored-by: Yury G. Kudryashov <urkud@urkud.name>
Co-authored-by: Bryan Gin-ge Chen <bryangingechen@gmail.com>
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers
No reviews
Assignees
No one assigned
Labels
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.

None yet
3 participants
@bryangingechen @robertylewis @jcommelin