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] - feat: port/CategoryTheory.Limits.Cones #2337

Closed
wants to merge 161 commits into from
Closed

[Merged by Bors] - feat: port/CategoryTheory.Limits.Cones #2337

wants to merge 161 commits into from

Conversation

mattrobball
Copy link
Collaborator

@mattrobball mattrobball commented Feb 17, 2023 •
edited by github-actions bot

hargoniX and others added 30 commits January 1, 2023 17:57
@hargoniX
Initial file copy from mathport
01c7d9e
@hargoniX
Mathbin -> Mathlib; add import to Mathlib.lean
bc9467d
@hargoniX
push it as far as possible
afd9aed
@Ruben-VandeVelde
Merge branch 'master' into port/CategoryTheory.Equivalence
c76b450
@mattrobball
seems to work
f0f6502
@mattrobball
add example and equivalence file for testing
91f541a
@thorimur
test: create slice.lean test file
92e65be
@mattrobball
Merge branch 'master' into port/CategoryTheory.Equivalence
afafdf0
@mattrobball
remove equivalence.lean
eedfb61
@mattrobball
remove rewriteTarget'; change MonadExceptOf to MonadExcept
ef7ef69
@mattrobball
add documentation and clean up
84ddfcb
@mattrobball
Merge branch 'master' into slice
adb9495
@mattrobball
move iteration tactics to core
3c369ce
@mattrobball
add slice to global import file
69bbb93
@mattrobball
modify documentation lines
319fa30
@mattrobball
add module documentation(?)
720d311
@mattrobball
minor changes
8256a85
@mattrobball
Merge branch 'slice' into port/CategoryTheory.Equivalence
88ac2d0
@mattrobball
fix module docs
388aaa0
@mattrobball
fix test/slice.lean
6bae31a
@mattrobball
Merge branch 'slice' into port/CategoryTheory.Equivalence
06c4b46
@mattrobball
fix all but refl error
7140d1c
@mattrobball
fix refl error and lint errors
2c8c8a7
@mattrobball
fix final long line
0c247c7
@thorimur
use Mathport syntax
2c56111 
* use existing docs
* fix docs typos
@thorimur
test: add simple rhs/lhs tests
80596f2
@thorimur
minor changes to Tactic.Core
ce383e4 
* use `m` instead of `TacticM` now that we use `MonadExcept`
* simplify code for `iterateRange`
* minor docs tweaks
@mattrobball
Merge branch 'slice' into port/CategoryTheory.Equivalence
cf945f0
@mattrobball
update slice naming
e6ec924
@mattrobball
Merge branch 'master' into port/CategoryTheory.Equivalence
68bcb25
@semorrison semorrison added the blocked-by-other-PR This PR depends on another PR which is still in the queue. label Feb 17, 2023
@mattrobball mattrobball removed the WIP Work in progress label Feb 18, 2023
@mattrobball mattrobball mentioned this pull request Feb 18, 2023
Closed
1 task
@semorrison semorrison added merge-conflict The PR has a merge conflict with master, and needs manual merging. and removed blocked-by-other-PR This PR depends on another PR which is still in the queue. labels Feb 18, 2023
@semorrison
Copy link
Contributor

This PR/issue depends on:

@mattrobball mattrobball added awaiting-review The author would like community review of the PR and removed merge-conflict The PR has a merge conflict with master, and needs manual merging. labels Feb 24, 2023
@jcommelin
Copy link
Member

These git histories are getting a bit out of hand for reviewing purposes. Do you think you can rebase some of these PRs on current master?

jcommelin
jcommelin approved these changes Feb 24, 2023
View reviewed changes
Copy link
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.

bors d+

@bors
Copy link

bors bot commented Feb 24, 2023

✌️ mattrobball can now approve this pull request. To approve and merge a pull request, simply reply with bors r+. More detailed instructions are available here.

@semorrison semorrison added delegated and removed awaiting-review The author would like community review of the PR labels Feb 24, 2023
@mattrobball
Copy link
Collaborator Author

bors merge

bors bot pushed a commit that referenced this pull request Feb 24, 2023
@hargoniX @Ruben-VandeVelde
@mattrobball @thorimur
feat: port/CategoryTheory.Limits.Cones (#2337)
332c3c9 
Co-authored-by: Ruben Van de Velde <65514131+Ruben-VandeVelde@users.noreply.github.com>
Co-authored-by: Matthew Ballard <matt@mrb.email>
Co-authored-by: thorimur <68410468+thorimur@users.noreply.github.com>
@bors
Copy link

bors bot commented Feb 24, 2023

Pull request successfully merged into master.

Build succeeded:

@bors bors bot changed the title feat: port/CategoryTheory.Limits.Cones [Merged by Bors] - feat: port/CategoryTheory.Limits.Cones Feb 24, 2023
@bors bors bot closed this Feb 24, 2023
@bors bors bot deleted the port/CategoryTheory.Limits.Cones branch February 24, 2023 20:08
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@jcommelin jcommelin jcommelin approved these changes

Assignees
No one assigned
Labels
delegated mathlib-port This is a port of a theory file from mathlib.
Projects
None yet
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.

None yet
9 participants
@mattrobball @semorrison @jcommelin @hargoniX @Ruben-VandeVelde @thorimur @mpenciak @adamtopaz @mo271