-
Notifications
You must be signed in to change notification settings - Fork 259
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.
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
[Merged by Bors] - feat: list permutations and pairwise #56
Conversation
There's some build errors here. But otherwise lgtm. bors d+ |
✌️ ammkrn can now approve this pull request. To approve and merge a pull request, simply reply with |
0dfb38a
to
987d492
Compare
The build errors should be fixed now. I changed the header of the commit message to |
The commit message is ignored by bors, only the PR title matters. |
bors r+ |
The only thing that isn't just an addition from mathlib is changing the binder on subset to a weak implicit.
Build failed: |
987d492
to
a615a1f
Compare
I can't tell from the ci what exactly is wrong; the only error I found just says a615a1f builds fine locally using |
You need to add the new file to diff --git a/Mathlib.lean b/Mathlib.lean
index 59a3af8..c64cf8a 100644
--- a/Mathlib.lean
+++ b/Mathlib.lean
@@ -10,6 +10,7 @@ import Mathlib.Data.Equiv.Functor
import Mathlib.Data.Int.Basic
import Mathlib.Data.List.Basic
import Mathlib.Data.List.Card
+import Mathlib.Data.List.Perm
import Mathlib.Data.Nat.Basic
import Mathlib.Data.Nat.Gcd
import Mathlib.Data.Prod |
a615a1f
to
af01cb6
Compare
bors r+ |
The only thing that isn't just an addition from mathlib is changing the binder on subset to a weak implicit.
Mmmh, this seems to be stuck: bors r- |
Canceled. |
The only thing that isn't just an addition from mathlib is changing the binder on subset to a weak implicit.
Pull request successfully merged into master. Build succeeded: |
Thanks for your patience. |
# This is the 1st commit message: automated fixes Mathbin -> Mathlib fix certain import statements move "by" to end of line add import to Mathlib.lean # The commit message #2 will be skipped: # feat: port CategoryTheory.Limits.IsLimit # The commit message #3 will be skipped: # Initial file copy from mathport # The commit message #4 will be skipped: # automated fixes # # Mathbin -> Mathlib # # fix certain import statements # # move "by" to end of line # # add import to Mathlib.lean # The commit message #5 will be skipped: # feat: port CategoryTheory.Limits.Cones # The commit message #6 will be skipped: # Initial file copy from mathport # The commit message #7 will be skipped: # automated fixes # # Mathbin -> Mathlib # # fix certain import statements # # move "by" to end of line # # add import to Mathlib.lean # The commit message #8 will be skipped: # feat: port CategoryTheory.Yoneda # The commit message #9 will be skipped: # Initial file copy from mathport # The commit message #10 will be skipped: # automated fixes # # Mathbin -> Mathlib # # fix certain import statements # # move "by" to end of line # # add import to Mathlib.lean # The commit message #11 will be skipped: # feat: port CategoryTheory.Functor.Currying # The commit message #12 will be skipped: # Initial file copy from mathport # The commit message #13 will be skipped: # automated fixes # # Mathbin -> Mathlib # # fix certain import statements # # move "by" to end of line # # add import to Mathlib.lean # The commit message #14 will be skipped: # fix all but one decl # The commit message #15 will be skipped: # fix last errors # The commit message #16 will be skipped: # feat: port CategoryTheory.Functor.Hom # The commit message #17 will be skipped: # Initial file copy from mathport # The commit message #18 will be skipped: # automated fixes # # Mathbin -> Mathlib # # fix certain import statements # # move "by" to end of line # # add import to Mathlib.lean # The commit message #19 will be skipped: # feat: port CategoryTheory.Types # The commit message #20 will be skipped: # Initial file copy from mathport # The commit message #21 will be skipped: # automated fixes # # Mathbin -> Mathlib # # fix certain import statements # # move "by" to end of line # # add import to Mathlib.lean # The commit message #22 will be skipped: # feat: port CategoryTheory.EpiMono # The commit message #23 will be skipped: # Initial file copy from mathport # The commit message #24 will be skipped: # automated fixes # # Mathbin -> Mathlib # # fix certain import statements # # move "by" to end of line # # add import to Mathlib.lean # The commit message #25 will be skipped: # feat: port CategoryTheory.Groupoid # The commit message #26 will be skipped: # Initial file copy from mathport # The commit message #27 will be skipped: # automated fixes # # Mathbin -> Mathlib # # fix certain import statements # # move "by" to end of line # # add import to Mathlib.lean # The commit message #28 will be skipped: # feat: port CategoryTheory.Pi.Basic # The commit message #29 will be skipped: # Initial file copy from mathport # The commit message #30 will be skipped: # automated fixes # # Mathbin -> Mathlib # # fix certain import statements # # move "by" to end of line # # add import to Mathlib.lean # The commit message #31 will be skipped: # fix some errors # The commit message #32 will be skipped: # some more fixes # The commit message #33 will be skipped: # more fixes # The commit message #34 will be skipped: # finally fixed # The commit message #35 will be skipped: # lint # The commit message #36 will be skipped: # add porting note for scary warning # The commit message #37 will be skipped: # add porting note about proliferation of match # The commit message #38 will be skipped: # initial pass # The commit message #39 will be skipped: # fix errors # The commit message #40 will be skipped: # lint # The commit message #41 will be skipped: # fix errors; lint; add porting notes # The commit message #42 will be skipped: # fix errors; lint; add porting note # The commit message #43 will be skipped: # fix error # The commit message #44 will be skipped: # fix some errors # The commit message #45 will be skipped: # minor fixes # The commit message #46 will be skipped: # fix all but four # The commit message #47 will be skipped: # fix last errors; lint # The commit message #48 will be skipped: # feat: port CategoryTheory.DiscreteCategory # The commit message #49 will be skipped: # Initial file copy from mathport # The commit message #50 will be skipped: # automated fixes # # Mathbin -> Mathlib # # fix certain import statements # # move "by" to end of line # # add import to Mathlib.lean # The commit message #51 will be skipped: # get file to build # The commit message #52 will be skipped: # lint # The commit message #53 will be skipped: # lint some more # The commit message #54 will be skipped: # feat: port CategoryTheory.Functor.ReflectsIsomorphisms # The commit message #55 will be skipped: # Initial file copy from mathport # The commit message #56 will be skipped: # automated fixes # # Mathbin -> Mathlib # # fix certain import statements # # move "by" to end of line # # add import to Mathlib.lean # The commit message #57 will be skipped: # feat: port CategoryTheory.Functor.EpiMono # The commit message #58 will be skipped: # Initial file copy from mathport # The commit message #59 will be skipped: # automated fixes # # Mathbin -> Mathlib # # fix certain import statements # # move "by" to end of line # # add import to Mathlib.lean # The commit message #60 will be skipped: # feat: port CategoryTheory.LiftingProperties.Adjunction # The commit message #61 will be skipped: # Initial file copy from mathport # The commit message #62 will be skipped: # automated fixes # # Mathbin -> Mathlib # # fix certain import statements # # move "by" to end of line # # add import to Mathlib.lean # The commit message #63 will be skipped: # feat: port CategoryTheory.LiftingProperties.Basic # The commit message #64 will be skipped: # Initial file copy from mathport # The commit message #65 will be skipped: # automated fixes # # Mathbin -> Mathlib # # fix certain import statements # # move "by" to end of line # # add import to Mathlib.lean # The commit message #66 will be skipped: # feat: port CategoryTheory.CommSq # The commit message #67 will be skipped: # Initial file copy from mathport # The commit message #68 will be skipped: # automated fixes # # Mathbin -> Mathlib # # fix certain import statements # # move "by" to end of line # # add import to Mathlib.lean # The commit message #69 will be skipped: # first pass # The commit message #70 will be skipped: # names and removing restate_axiom # The commit message #71 will be skipped: # fix lint # The commit message #72 will be skipped: # remove spurious edit # The commit message #73 will be skipped: # fix errors; lint # The commit message #74 will be skipped: # feat: port CategoryTheory.Adjunction.Basic # The commit message #75 will be skipped: # Initial file copy from mathport # The commit message #76 will be skipped: # automated fixes # # Mathbin -> Mathlib # # fix certain import statements # # move "by" to end of line # # add import to Mathlib.lean # The commit message #77 will be skipped: # Initial file copy from mathport # The commit message #78 will be skipped: # Mathbin -> Mathlib; add import to Mathlib.lean # The commit message #79 will be skipped: # push it as far as possible # The commit message #80 will be skipped: # minor changes # The commit message #81 will be skipped: # seems to work # The commit message #82 will be skipped: # add example and equivalence file for testing # The commit message #83 will be skipped: # test: create `slice.lean` test file # The commit message #84 will be skipped: # remove equivalence.lean # The commit message #85 will be skipped: # remove rewriteTarget'; change MonadExceptOf to MonadExcept # The commit message #86 will be skipped: # add documentation and clean up # The commit message #87 will be skipped: # move iteration tactics to core # The commit message #88 will be skipped: # modify documentation lines # The commit message #89 will be skipped: # add module documentation(?) # The commit message #90 will be skipped: # fix module docs # The commit message #91 will be skipped: # fix test/slice.lean # The commit message #92 will be skipped: # fix all but refl error # The commit message #93 will be skipped: # fix refl error and lint errors # The commit message #94 will be skipped: # fix final long line # The commit message #95 will be skipped: # use `Mathport` syntax # * use existing docs # * fix docs typos # The commit message #96 will be skipped: # test: add simple `rhs`/`lhs` tests # The commit message #97 will be skipped: # minor changes to `Tactic.Core` # * use `m` instead of `TacticM` now that we use `MonadExcept` # * simplify code for `iterateRange` # * minor docs tweaks # The commit message #98 will be skipped: # update slice naming # The commit message #99 will be skipped: # some progress # The commit message #100 will be skipped: # only one error left # The commit message #101 will be skipped: # filled in last sorry # The commit message #102 will be skipped: # break long lines # The commit message #103 will be skipped: # delete linter command # The commit message #104 will be skipped: # fix comments # The commit message #105 will be skipped: # fix two simpNF lints # The commit message #106 will be skipped: # fill in some docstrings # The commit message #107 will be skipped: # fix most linter issues # The commit message #108 will be skipped: # add missing aligns for fields; lint # The commit message #109 will be skipped: # restore lost import line # The commit message #110 will be skipped: # fix errors; lint # The commit message #111 will be skipped: # feat: port CategoryTheory.Limits.Shapes.StrongEpi # The commit message #112 will be skipped: # Initial file copy from mathport # The commit message #113 will be skipped: # automated fixes # # Mathbin -> Mathlib # # fix certain import statements # # move "by" to end of line # # add import to Mathlib.lean # The commit message #114 will be skipped: # fix errors; lint # The commit message #115 will be skipped: # Update Mathlib.lean # The commit message #116 will be skipped: # fix errors; lint # The commit message #117 will be skipped: # fix errors; lint; shorten filename # The commit message #118 will be skipped: # fix some errors # The commit message #119 will be skipped: # fix some more # The commit message #120 will be skipped: # fix errors # The commit message #121 will be skipped: # lint # The commit message #122 will be skipped: # fix errors # The commit message #123 will be skipped: # lint # The commit message #124 will be skipped: # feat: port CategoryTheory.Category.Ulift # The commit message #125 will be skipped: # Initial file copy from mathport # The commit message #126 will be skipped: # automated fixes # # Mathbin -> Mathlib # # fix certain import statements # # move "by" to end of line # # add import to Mathlib.lean
# This is the 1st commit message: automated fixes Mathbin -> Mathlib fix certain import statements move "by" to end of line add import to Mathlib.lean # The commit message #2 will be skipped: # feat: port CategoryTheory.Limits.Cones # The commit message #3 will be skipped: # Initial file copy from mathport # The commit message #4 will be skipped: # automated fixes # # Mathbin -> Mathlib # # fix certain import statements # # move "by" to end of line # # add import to Mathlib.lean # The commit message #5 will be skipped: # feat: port CategoryTheory.Yoneda # The commit message #6 will be skipped: # Initial file copy from mathport # The commit message #7 will be skipped: # automated fixes # # Mathbin -> Mathlib # # fix certain import statements # # move "by" to end of line # # add import to Mathlib.lean # The commit message #8 will be skipped: # feat: port CategoryTheory.Functor.Currying # The commit message #9 will be skipped: # Initial file copy from mathport # The commit message #10 will be skipped: # automated fixes # # Mathbin -> Mathlib # # fix certain import statements # # move "by" to end of line # # add import to Mathlib.lean # The commit message #11 will be skipped: # fix all but one decl # The commit message #12 will be skipped: # fix last errors # The commit message #13 will be skipped: # feat: port CategoryTheory.Functor.Hom # The commit message #14 will be skipped: # Initial file copy from mathport # The commit message #15 will be skipped: # automated fixes # # Mathbin -> Mathlib # # fix certain import statements # # move "by" to end of line # # add import to Mathlib.lean # The commit message #16 will be skipped: # feat: port CategoryTheory.Types # The commit message #17 will be skipped: # Initial file copy from mathport # The commit message #18 will be skipped: # automated fixes # # Mathbin -> Mathlib # # fix certain import statements # # move "by" to end of line # # add import to Mathlib.lean # The commit message #19 will be skipped: # feat: port CategoryTheory.EpiMono # The commit message #20 will be skipped: # Initial file copy from mathport # The commit message #21 will be skipped: # automated fixes # # Mathbin -> Mathlib # # fix certain import statements # # move "by" to end of line # # add import to Mathlib.lean # The commit message #22 will be skipped: # feat: port CategoryTheory.Groupoid # The commit message #23 will be skipped: # Initial file copy from mathport # The commit message #24 will be skipped: # automated fixes # # Mathbin -> Mathlib # # fix certain import statements # # move "by" to end of line # # add import to Mathlib.lean # The commit message #25 will be skipped: # feat: port CategoryTheory.Pi.Basic # The commit message #26 will be skipped: # Initial file copy from mathport # The commit message #27 will be skipped: # automated fixes # # Mathbin -> Mathlib # # fix certain import statements # # move "by" to end of line # # add import to Mathlib.lean # The commit message #28 will be skipped: # fix some errors # The commit message #29 will be skipped: # some more fixes # The commit message #30 will be skipped: # more fixes # The commit message #31 will be skipped: # finally fixed # The commit message #32 will be skipped: # lint # The commit message #33 will be skipped: # add porting note for scary warning # The commit message #34 will be skipped: # add porting note about proliferation of match # The commit message #35 will be skipped: # initial pass # The commit message #36 will be skipped: # fix errors # The commit message #37 will be skipped: # lint # The commit message #38 will be skipped: # fix errors; lint; add porting notes # The commit message #39 will be skipped: # fix errors; lint; add porting note # The commit message #40 will be skipped: # fix error # The commit message #41 will be skipped: # fix some errors # The commit message #42 will be skipped: # minor fixes # The commit message #43 will be skipped: # fix all but four # The commit message #44 will be skipped: # Delete start_port-macos.sh # The commit message #45 will be skipped: # fix last errors; lint # The commit message #46 will be skipped: # feat: port CategoryTheory.DiscreteCategory # The commit message #47 will be skipped: # Initial file copy from mathport # The commit message #48 will be skipped: # automated fixes # # Mathbin -> Mathlib # # fix certain import statements # # move "by" to end of line # # add import to Mathlib.lean # The commit message #49 will be skipped: # get file to build # The commit message #50 will be skipped: # lint # The commit message #51 will be skipped: # lint some more # The commit message #52 will be skipped: # feat: port CategoryTheory.Functor.ReflectsIsomorphisms # The commit message #53 will be skipped: # Initial file copy from mathport # The commit message #54 will be skipped: # automated fixes # # Mathbin -> Mathlib # # fix certain import statements # # move "by" to end of line # # add import to Mathlib.lean # The commit message #55 will be skipped: # feat: port CategoryTheory.Functor.EpiMono # The commit message #56 will be skipped: # Initial file copy from mathport # The commit message #57 will be skipped: # automated fixes # # Mathbin -> Mathlib # # fix certain import statements # # move "by" to end of line # # add import to Mathlib.lean # The commit message #58 will be skipped: # feat: port CategoryTheory.LiftingProperties.Adjunction # The commit message #59 will be skipped: # Initial file copy from mathport # The commit message #60 will be skipped: # automated fixes # # Mathbin -> Mathlib # # fix certain import statements # # move "by" to end of line # # add import to Mathlib.lean # The commit message #61 will be skipped: # feat: port CategoryTheory.LiftingProperties.Basic # The commit message #62 will be skipped: # Initial file copy from mathport # The commit message #63 will be skipped: # automated fixes # # Mathbin -> Mathlib # # fix certain import statements # # move "by" to end of line # # add import to Mathlib.lean # The commit message #64 will be skipped: # feat: port CategoryTheory.CommSq # The commit message #65 will be skipped: # Initial file copy from mathport # The commit message #66 will be skipped: # automated fixes # # Mathbin -> Mathlib # # fix certain import statements # # move "by" to end of line # # add import to Mathlib.lean # The commit message #67 will be skipped: # first pass # The commit message #68 will be skipped: # names and removing restate_axiom # The commit message #69 will be skipped: # fix lint # The commit message #70 will be skipped: # remove spurious edit # The commit message #71 will be skipped: # fix errors; lint # The commit message #72 will be skipped: # feat: port CategoryTheory.Adjunction.Basic # The commit message #73 will be skipped: # Initial file copy from mathport # The commit message #74 will be skipped: # automated fixes # # Mathbin -> Mathlib # # fix certain import statements # # move "by" to end of line # # add import to Mathlib.lean # The commit message #75 will be skipped: # Initial file copy from mathport # The commit message #76 will be skipped: # Mathbin -> Mathlib; add import to Mathlib.lean # The commit message #77 will be skipped: # push it as far as possible # The commit message #78 will be skipped: # minor changes # The commit message #79 will be skipped: # seems to work # The commit message #80 will be skipped: # add example and equivalence file for testing # The commit message #81 will be skipped: # test: create `slice.lean` test file # The commit message #82 will be skipped: # remove equivalence.lean # The commit message #83 will be skipped: # remove rewriteTarget'; change MonadExceptOf to MonadExcept # The commit message #84 will be skipped: # add documentation and clean up # The commit message #85 will be skipped: # move iteration tactics to core # The commit message #86 will be skipped: # add slice to global import file # The commit message #87 will be skipped: # modify documentation lines # The commit message #88 will be skipped: # add module documentation(?) # The commit message #89 will be skipped: # fix module docs # The commit message #90 will be skipped: # fix test/slice.lean
commit 6a44854 Author: Matthew Ballard <matt@mrb.email> Date: Tue Feb 28 06:29:46 2023 -0500 add missing aligns to cones.lean commit 84ea4c6 Author: Matthew Ballard <matt@mrb.email> Date: Mon Feb 27 14:55:26 2023 -0500 lint for changes and clean up commit 3ef0e8b Author: Matthew Ballard <matt@mrb.email> Date: Mon Feb 27 14:12:15 2023 -0500 golf (co)yoneda proofs commit 16bd36d Author: Matthew Ballard <matt@mrb.email> Date: Mon Feb 27 12:53:09 2023 -0500 remove extra instances commit 21f6296 Merge: 1985f48 5107462 Author: Matthew Ballard <matt@mrb.email> Date: Mon Feb 27 06:47:34 2023 -0500 Merge branch 'master' into port/CategoryTheory.Limits.HasLimits commit 1985f48 Author: Matthew Ballard <matt@mrb.email> Date: Mon Feb 27 06:46:53 2023 -0500 add updated dependencies commit d862b81 Author: Matthew Ballard <matt@mrb.email> Date: Fri Feb 24 21:42:30 2023 -0500 fix long line commit 51660c6 Author: Matthew Ballard <matt@mrb.email> Date: Fri Feb 24 21:39:24 2023 -0500 change X to pt commit e708679 Author: Matthew Ballard <matt@mrb.email> Date: Fri Feb 24 21:30:52 2023 -0500 revert one more commit 69b5d00 Author: Matthew Ballard <matt@mrb.email> Date: Fri Feb 24 21:30:10 2023 -0500 fix rebase commit 5f289c1 Author: Matthew Ballard <matt@mrb.email> Date: Fri Feb 24 20:52:34 2023 -0500 fix import file commit d3d56ee Author: Matthew Ballard <matt@mrb.email> Date: Tue Feb 21 23:16:12 2023 -0500 move names to new convention commit 9dfd1d9 Author: Matthew Ballard <matt@mrb.email> Date: Tue Feb 21 23:02:58 2023 -0500 add updated files commit 90d60fc Author: Matthew Ballard <matt@mrb.email> Date: Sun Feb 19 19:19:52 2023 -0500 fix case error commit 6979193 Author: Matthew Ballard <matt@mrb.email> Date: Sun Feb 19 00:02:32 2023 -0500 fix import line typo commit 843cf69 Author: Matthew Ballard <matt@mrb.email> Date: Sat Feb 18 23:52:06 2023 -0500 fix import file commit 4534cda Author: Matthew Ballard <matt@mrb.email> Date: Sat Feb 18 23:51:22 2023 -0500 align names in comments commit 4dfea81 Author: Matthew Ballard <matt@mrb.email> Date: Sat Feb 18 23:38:31 2023 -0500 lint for CI commit 6373462 Author: Matthew Ballard <matt@mrb.email> Date: Sat Feb 18 23:28:31 2023 -0500 try fix-comments.py only fixed a single issue for the second time now commit a45d823 Author: Matthew Ballard <matt@mrb.email> Date: Sat Feb 18 23:26:14 2023 -0500 fix final error commit f7dcf96 Author: Matthew Ballard <matt@mrb.email> Date: Sat Feb 18 23:22:54 2023 -0500 fix all but one decl commit 2f25984 Author: Matthew Ballard <matt@mrb.email> Date: Fri Feb 24 20:50:11 2023 -0500 automated fixes Mathbin -> Mathlib fix certain import statements move "by" to end of line add import to Mathlib.lean commit f1c2148 Author: Matthew Ballard <matt@mrb.email> Date: Fri Feb 24 20:49:48 2023 -0500 automated fixes Mathbin -> Mathlib fix certain import statements move "by" to end of line add import to Mathlib.lean commit 8fcb216 Author: Matthew Ballard <matt@mrb.email> Date: Sat Feb 18 21:19:06 2023 -0500 # This is a combination of 126 commits. # This is the 1st commit message: automated fixes Mathbin -> Mathlib fix certain import statements move "by" to end of line add import to Mathlib.lean # The commit message #2 will be skipped: # feat: port CategoryTheory.Limits.IsLimit # The commit message #3 will be skipped: # Initial file copy from mathport # The commit message #4 will be skipped: # automated fixes # # Mathbin -> Mathlib # # fix certain import statements # # move "by" to end of line # # add import to Mathlib.lean # The commit message #5 will be skipped: # feat: port CategoryTheory.Limits.Cones # The commit message #6 will be skipped: # Initial file copy from mathport # The commit message #7 will be skipped: # automated fixes # # Mathbin -> Mathlib # # fix certain import statements # # move "by" to end of line # # add import to Mathlib.lean # The commit message #8 will be skipped: # feat: port CategoryTheory.Yoneda # The commit message #9 will be skipped: # Initial file copy from mathport # The commit message #10 will be skipped: # automated fixes # # Mathbin -> Mathlib # # fix certain import statements # # move "by" to end of line # # add import to Mathlib.lean # The commit message #11 will be skipped: # feat: port CategoryTheory.Functor.Currying # The commit message #12 will be skipped: # Initial file copy from mathport # The commit message #13 will be skipped: # automated fixes # # Mathbin -> Mathlib # # fix certain import statements # # move "by" to end of line # # add import to Mathlib.lean # The commit message #14 will be skipped: # fix all but one decl # The commit message #15 will be skipped: # fix last errors # The commit message #16 will be skipped: # feat: port CategoryTheory.Functor.Hom # The commit message #17 will be skipped: # Initial file copy from mathport # The commit message #18 will be skipped: # automated fixes # # Mathbin -> Mathlib # # fix certain import statements # # move "by" to end of line # # add import to Mathlib.lean # The commit message #19 will be skipped: # feat: port CategoryTheory.Types # The commit message #20 will be skipped: # Initial file copy from mathport # The commit message #21 will be skipped: # automated fixes # # Mathbin -> Mathlib # # fix certain import statements # # move "by" to end of line # # add import to Mathlib.lean # The commit message #22 will be skipped: # feat: port CategoryTheory.EpiMono # The commit message #23 will be skipped: # Initial file copy from mathport # The commit message #24 will be skipped: # automated fixes # # Mathbin -> Mathlib # # fix certain import statements # # move "by" to end of line # # add import to Mathlib.lean # The commit message #25 will be skipped: # feat: port CategoryTheory.Groupoid # The commit message #26 will be skipped: # Initial file copy from mathport # The commit message #27 will be skipped: # automated fixes # # Mathbin -> Mathlib # # fix certain import statements # # move "by" to end of line # # add import to Mathlib.lean # The commit message #28 will be skipped: # feat: port CategoryTheory.Pi.Basic # The commit message #29 will be skipped: # Initial file copy from mathport # The commit message #30 will be skipped: # automated fixes # # Mathbin -> Mathlib # # fix certain import statements # # move "by" to end of line # # add import to Mathlib.lean # The commit message #31 will be skipped: # fix some errors # The commit message #32 will be skipped: # some more fixes # The commit message #33 will be skipped: # more fixes # The commit message #34 will be skipped: # finally fixed # The commit message #35 will be skipped: # lint # The commit message #36 will be skipped: # add porting note for scary warning # The commit message #37 will be skipped: # add porting note about proliferation of match # The commit message #38 will be skipped: # initial pass # The commit message #39 will be skipped: # fix errors # The commit message #40 will be skipped: # lint # The commit message #41 will be skipped: # fix errors; lint; add porting notes # The commit message #42 will be skipped: # fix errors; lint; add porting note # The commit message #43 will be skipped: # fix error # The commit message #44 will be skipped: # fix some errors # The commit message #45 will be skipped: # minor fixes # The commit message #46 will be skipped: # fix all but four # The commit message #47 will be skipped: # fix last errors; lint # The commit message #48 will be skipped: # feat: port CategoryTheory.DiscreteCategory # The commit message #49 will be skipped: # Initial file copy from mathport # The commit message #50 will be skipped: # automated fixes # # Mathbin -> Mathlib # # fix certain import statements # # move "by" to end of line # # add import to Mathlib.lean # The commit message #51 will be skipped: # get file to build # The commit message #52 will be skipped: # lint # The commit message #53 will be skipped: # lint some more # The commit message #54 will be skipped: # feat: port CategoryTheory.Functor.ReflectsIsomorphisms # The commit message #55 will be skipped: # Initial file copy from mathport # The commit message #56 will be skipped: # automated fixes # # Mathbin -> Mathlib # # fix certain import statements # # move "by" to end of line # # add import to Mathlib.lean # The commit message #57 will be skipped: # feat: port CategoryTheory.Functor.EpiMono # The commit message #58 will be skipped: # Initial file copy from mathport # The commit message #59 will be skipped: # automated fixes # # Mathbin -> Mathlib # # fix certain import statements # # move "by" to end of line # # add import to Mathlib.lean # The commit message #60 will be skipped: # feat: port CategoryTheory.LiftingProperties.Adjunction # The commit message #61 will be skipped: # Initial file copy from mathport # The commit message #62 will be skipped: # automated fixes # # Mathbin -> Mathlib # # fix certain import statements # # move "by" to end of line # # add import to Mathlib.lean # The commit message #63 will be skipped: # feat: port CategoryTheory.LiftingProperties.Basic # The commit message #64 will be skipped: # Initial file copy from mathport # The commit message #65 will be skipped: # automated fixes # # Mathbin -> Mathlib # # fix certain import statements # # move "by" to end of line # # add import to Mathlib.lean # The commit message #66 will be skipped: # feat: port CategoryTheory.CommSq # The commit message #67 will be skipped: # Initial file copy from mathport # The commit message #68 will be skipped: # automated fixes # # Mathbin -> Mathlib # # fix certain import statements # # move "by" to end of line # # add import to Mathlib.lean # The commit message #69 will be skipped: # first pass # The commit message #70 will be skipped: # names and removing restate_axiom # The commit message #71 will be skipped: # fix lint # The commit message #72 will be skipped: # remove spurious edit # The commit message #73 will be skipped: # fix errors; lint # The commit message #74 will be skipped: # feat: port CategoryTheory.Adjunction.Basic # The commit message #75 will be skipped: # Initial file copy from mathport # The commit message #76 will be skipped: # automated fixes # # Mathbin -> Mathlib # # fix certain import statements # # move "by" to end of line # # add import to Mathlib.lean # The commit message #77 will be skipped: # Initial file copy from mathport # The commit message #78 will be skipped: # Mathbin -> Mathlib; add import to Mathlib.lean # The commit message #79 will be skipped: # push it as far as possible # The commit message #80 will be skipped: # minor changes # The commit message #81 will be skipped: # seems to work # The commit message #82 will be skipped: # add example and equivalence file for testing # The commit message #83 will be skipped: # test: create `slice.lean` test file # The commit message #84 will be skipped: # remove equivalence.lean # The commit message #85 will be skipped: # remove rewriteTarget'; change MonadExceptOf to MonadExcept # The commit message #86 will be skipped: # add documentation and clean up # The commit message #87 will be skipped: # move iteration tactics to core # The commit message #88 will be skipped: # modify documentation lines # The commit message #89 will be skipped: # add module documentation(?) # The commit message #90 will be skipped: # fix module docs # The commit message #91 will be skipped: # fix test/slice.lean # The commit message #92 will be skipped: # fix all but refl error # The commit message #93 will be skipped: # fix refl error and lint errors # The commit message #94 will be skipped: # fix final long line # The commit message #95 will be skipped: # use `Mathport` syntax # * use existing docs # * fix docs typos # The commit message #96 will be skipped: # test: add simple `rhs`/`lhs` tests # The commit message #97 will be skipped: # minor changes to `Tactic.Core` # * use `m` instead of `TacticM` now that we use `MonadExcept` # * simplify code for `iterateRange` # * minor docs tweaks # The commit message #98 will be skipped: # update slice naming # The commit message #99 will be skipped: # some progress # The commit message #100 will be skipped: # only one error left # The commit message #101 will be skipped: # filled in last sorry # The commit message #102 will be skipped: # break long lines # The commit message #103 will be skipped: # delete linter command # The commit message #104 will be skipped: # fix comments # The commit message #105 will be skipped: # fix two simpNF lints # The commit message #106 will be skipped: # fill in some docstrings # The commit message #107 will be skipped: # fix most linter issues # The commit message #108 will be skipped: # add missing aligns for fields; lint # The commit message #109 will be skipped: # restore lost import line # The commit message #110 will be skipped: # fix errors; lint # The commit message #111 will be skipped: # feat: port CategoryTheory.Limits.Shapes.StrongEpi # The commit message #112 will be skipped: # Initial file copy from mathport # The commit message #113 will be skipped: # automated fixes # # Mathbin -> Mathlib # # fix certain import statements # # move "by" to end of line # # add import to Mathlib.lean # The commit message #114 will be skipped: # fix errors; lint # The commit message #115 will be skipped: # Update Mathlib.lean # The commit message #116 will be skipped: # fix errors; lint # The commit message #117 will be skipped: # fix errors; lint; shorten filename # The commit message #118 will be skipped: # fix some errors # The commit message #119 will be skipped: # fix some more # The commit message #120 will be skipped: # fix errors # The commit message #121 will be skipped: # lint # The commit message #122 will be skipped: # fix errors # The commit message #123 will be skipped: # lint # The commit message #124 will be skipped: # feat: port CategoryTheory.Category.Ulift # The commit message #125 will be skipped: # Initial file copy from mathport # The commit message #126 will be skipped: # automated fixes # # Mathbin -> Mathlib # # fix certain import statements # # move "by" to end of line # # add import to Mathlib.lean commit e22a9d9 Author: Matthew Ballard <matt@mrb.email> Date: Sat Feb 18 21:19:06 2023 -0500 Initial file copy from mathport commit f875c67 Author: Matthew Ballard <matt@mrb.email> Date: Sat Feb 18 21:19:06 2023 -0500 feat: port CategoryTheory.Limits.HasLimits
# This is the 1st commit message: automated fixes Mathbin -> Mathlib fix certain import statements move "by" to end of line add import to Mathlib.lean # The commit message #2 will be skipped: # feat: port CategoryTheory.Limits.HasLimits # The commit message #3 will be skipped: # Initial file copy from mathport # The commit message #4 will be skipped: # automated fixes # # Mathbin -> Mathlib # # fix certain import statements # # move "by" to end of line # # add import to Mathlib.lean # The commit message #5 will be skipped: # feat: port CategoryTheory.Limits.IsLimit # The commit message #6 will be skipped: # Initial file copy from mathport # The commit message #7 will be skipped: # automated fixes # # Mathbin -> Mathlib # # fix certain import statements # # move "by" to end of line # # add import to Mathlib.lean # The commit message #8 will be skipped: # feat: port CategoryTheory.Limits.Cones # The commit message #9 will be skipped: # Initial file copy from mathport # The commit message #10 will be skipped: # automated fixes # # Mathbin -> Mathlib # # fix certain import statements # # move "by" to end of line # # add import to Mathlib.lean # The commit message #11 will be skipped: # feat: port CategoryTheory.Yoneda # The commit message #12 will be skipped: # Initial file copy from mathport # The commit message #13 will be skipped: # automated fixes # # Mathbin -> Mathlib # # fix certain import statements # # move "by" to end of line # # add import to Mathlib.lean # The commit message #14 will be skipped: # feat: port CategoryTheory.Functor.Currying # The commit message #15 will be skipped: # Initial file copy from mathport # The commit message #16 will be skipped: # automated fixes # # Mathbin -> Mathlib # # fix certain import statements # # move "by" to end of line # # add import to Mathlib.lean # The commit message #17 will be skipped: # fix all but one decl # The commit message #18 will be skipped: # fix last errors # The commit message #19 will be skipped: # feat: port CategoryTheory.Functor.Hom # The commit message #20 will be skipped: # Initial file copy from mathport # The commit message #21 will be skipped: # automated fixes # # Mathbin -> Mathlib # # fix certain import statements # # move "by" to end of line # # add import to Mathlib.lean # The commit message #22 will be skipped: # feat: port CategoryTheory.Types # The commit message #23 will be skipped: # Initial file copy from mathport # The commit message #24 will be skipped: # automated fixes # # Mathbin -> Mathlib # # fix certain import statements # # move "by" to end of line # # add import to Mathlib.lean # The commit message #25 will be skipped: # feat: port CategoryTheory.EpiMono # The commit message #26 will be skipped: # Initial file copy from mathport # The commit message #27 will be skipped: # automated fixes # # Mathbin -> Mathlib # # fix certain import statements # # move "by" to end of line # # add import to Mathlib.lean # The commit message #28 will be skipped: # feat: port CategoryTheory.Groupoid # The commit message #29 will be skipped: # Initial file copy from mathport # The commit message #30 will be skipped: # automated fixes # # Mathbin -> Mathlib # # fix certain import statements # # move "by" to end of line # # add import to Mathlib.lean # The commit message #31 will be skipped: # feat: port CategoryTheory.Pi.Basic # The commit message #32 will be skipped: # Initial file copy from mathport # The commit message #33 will be skipped: # automated fixes # # Mathbin -> Mathlib # # fix certain import statements # # move "by" to end of line # # add import to Mathlib.lean # The commit message #34 will be skipped: # fix some errors # The commit message #35 will be skipped: # some more fixes # The commit message #36 will be skipped: # more fixes # The commit message #37 will be skipped: # finally fixed # The commit message #38 will be skipped: # lint # The commit message #39 will be skipped: # add porting note for scary warning # The commit message #40 will be skipped: # add porting note about proliferation of match # The commit message #41 will be skipped: # initial pass # The commit message #42 will be skipped: # fix errors # The commit message #43 will be skipped: # lint # The commit message #44 will be skipped: # fix errors; lint; add porting notes # The commit message #45 will be skipped: # fix errors; lint; add porting note # The commit message #46 will be skipped: # fix error # The commit message #47 will be skipped: # fix some errors # The commit message #48 will be skipped: # minor fixes # The commit message #49 will be skipped: # fix all but four # The commit message #50 will be skipped: # Delete start_port-macos.sh # The commit message #51 will be skipped: # fix last errors; lint # The commit message #52 will be skipped: # feat: port CategoryTheory.DiscreteCategory # The commit message #53 will be skipped: # Initial file copy from mathport # The commit message #54 will be skipped: # automated fixes # # Mathbin -> Mathlib # # fix certain import statements # # move "by" to end of line # # add import to Mathlib.lean # The commit message #55 will be skipped: # get file to build # The commit message #56 will be skipped: # lint # The commit message #57 will be skipped: # lint some more # The commit message #58 will be skipped: # feat: port CategoryTheory.Functor.ReflectsIsomorphisms # The commit message #59 will be skipped: # Initial file copy from mathport # The commit message #60 will be skipped: # automated fixes # # Mathbin -> Mathlib # # fix certain import statements # # move "by" to end of line # # add import to Mathlib.lean # The commit message #61 will be skipped: # feat: port CategoryTheory.Functor.EpiMono # The commit message #62 will be skipped: # Initial file copy from mathport # The commit message #63 will be skipped: # automated fixes # # Mathbin -> Mathlib # # fix certain import statements # # move "by" to end of line # # add import to Mathlib.lean # The commit message #64 will be skipped: # feat: port CategoryTheory.LiftingProperties.Adjunction # The commit message #65 will be skipped: # Initial file copy from mathport # The commit message #66 will be skipped: # automated fixes # # Mathbin -> Mathlib # # fix certain import statements # # move "by" to end of line # # add import to Mathlib.lean # The commit message #67 will be skipped: # feat: port CategoryTheory.LiftingProperties.Basic # The commit message #68 will be skipped: # Initial file copy from mathport # The commit message #69 will be skipped: # automated fixes # # Mathbin -> Mathlib # # fix certain import statements # # move "by" to end of line # # add import to Mathlib.lean # The commit message #70 will be skipped: # feat: port CategoryTheory.CommSq # The commit message #71 will be skipped: # Initial file copy from mathport # The commit message #72 will be skipped: # automated fixes # # Mathbin -> Mathlib # # fix certain import statements # # move "by" to end of line # # add import to Mathlib.lean # The commit message #73 will be skipped: # first pass # The commit message #74 will be skipped: # names and removing restate_axiom # The commit message #75 will be skipped: # fix lint # The commit message #76 will be skipped: # remove spurious edit # The commit message #77 will be skipped: # fix errors; lint # The commit message #78 will be skipped: # feat: port CategoryTheory.Adjunction.Basic # The commit message #79 will be skipped: # Initial file copy from mathport # The commit message #80 will be skipped: # automated fixes # # Mathbin -> Mathlib # # fix certain import statements # # move "by" to end of line # # add import to Mathlib.lean # The commit message #81 will be skipped: # Initial file copy from mathport # The commit message #82 will be skipped: # Mathbin -> Mathlib; add import to Mathlib.lean # The commit message #83 will be skipped: # push it as far as possible # The commit message #84 will be skipped: # minor changes # The commit message #85 will be skipped: # seems to work # The commit message #86 will be skipped: # add example and equivalence file for testing # The commit message #87 will be skipped: # test: create `slice.lean` test file
The only thing that isn't just an addition from mathlib is changing the binder on subset to a weak implicit.