feat(Data/Int): port data.int.basic from the lean3 prelude #23
Conversation
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
kbuzzard
reviewed
Jul 3, 2021
Honestly I'm clueless as to what the Lean 4 naming convention is, or if there even is one. I just made snake_case aliases for things because that's what Nat.Basic does and left everything else the same as lean3. Do you know if there's some kind of document or zulip thread I can read that will clarify it a little? |
|
The main zulip thread on the topic is https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/rfc.3A.20theorem.20names . I was pretty happy with the proposal here and it seemed to be gaining traction until Leo vetoed it in the final hour, and the discussion hasn't progressed since then. Lean 4 core has a mashup of naming conventions, because the convention changed over time and the old stuff (especially proofs) was not updated. Those snake_case aliases are my attempt to bring some order to the madness with the naming convention called "proposal 3" in the thread: PascalCase namespaces, modules, and types, javaCase functions, and snake_case theorems. The proposal variation of uncertain outcome is whether to javaCase propositions as well. |
|
I'll add that I also like Mario's proposal. |
bryangingechen
changed the title
|
@denayd Git reports a conflict when I try to rebase and merge. Could you rebase and fix it, and then I'll merge? |
|
@denayd Oh, I could squash-and-merge -- never mind. Sorry for the noise. |
mattrobball
added a commit
that referenced
this pull request
Feb 25, 2023
# 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
mattrobball
added a commit
that referenced
this pull request
Feb 25, 2023
# 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
mattrobball
added a commit
that referenced
this pull request
Mar 1, 2023
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
mattrobball
added a commit
that referenced
this pull request
Mar 1, 2023
# 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
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
I needed some facts about the integers and Lean4 core just defines them and leaves it at that. This file proves the ring properties, provides some lemmas about the Nat to Int coercion, and defines a couple extra functions like sign and gcd.
It has to slightly modify Algebra.Group.Defs because that also defines the ℤ notation
Next up: my port of Data.Int.Order which depends on #18