[Merged by Bors] - feat(Data/UInt, Data/Fin/Basic) declarations #90
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
Add new Fin instances, extend the UInt declarations to other UInt types using a macro. This incorporates @gebner's suggestions to add boolean methods for checking under/overflow, and adding separate instances of `Fin size`. I still can't figure out the elaboration issue mentioned [here on zulip](https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/simp.20type.20annotations/near/260877092), so I can't use the macro on USize yet.
gebner
reviewed
Nov 13, 2021
Mathlib/Data/Fin/Basic.lean
Outdated
| instance : Neg (Fin n) where | ||
| neg a := ⟨(n - a) % n, Nat.mod_lt _ (lt_of_le_of_lt (Nat.zero_le _) a.isLt)⟩ | ||
| lemma Fin.mul_assoc (a b c : Fin n) : (a * b) * c = a * (b * c) := by | ||
| apply Fin.eq_of_val_eq |
There was a problem hiding this comment.
The mathlib proof in Lean 3 seems to be much shorter: https://github.com/leanprover-community/mathlib/blob/3578403f0c5cfbef907d1632ee91cee4b3cc6596/src/data/zmod/basic.lean#L47-L49
semorrison
added
the
awaiting-author
|
I'm working your suggestions in; I've also been trying to figure out the most comfortable way to work around the |
That should work as well. Is there a reason my suggestion at the lean issue doesn't work, i.e.? instance : CommRing (Fin USize.size) := inferInstanceAs (CommRing (Fin (_ + 1)))That still seems like the easiest solution to me and doesn't require changing anything else. |
gebner
reviewed
Nov 16, 2021
Switch over to using the `[Inhabited (Fin n)]` bound, inilne lemmas where possible, and add USize. The Inhabited bound is needed to deal with the combination of `USize.size` not being defined in terms of `Nat.succ`, and `Zero` not giving enough information (by itself) to prove the lemmas needed for classes like AddMonoid. We need to know that `0` from OfNat.ofNat is definitionally equal to something that actually has the requisite properties.
gebner
reviewed
Nov 17, 2021
Mathlib/Data/UInt.lean
Outdated
Comment on lines
94
to
97
| lemma val_zero : (0 : $typeName).val = (0 : Fin size) := by | ||
| delta OfNat.ofNat | ||
| delta $deltaName | ||
| simp only [ofNat, instOfNat, Zero.zero] |
There was a problem hiding this comment.
Suggested change
| lemma val_zero : (0 : $typeName).val = (0 : Fin size) := by | |
| delta OfNat.ofNat | |
| delta $deltaName | |
| simp only [ofNat, instOfNat, Zero.zero] | |
| lemma val_zero : (0 : $typeName).val = (0 : Fin size) := rfl |
The two zeroes here should absolutely be definitionally equal, and indeed they are.
Mathlib/Data/UInt.lean
Outdated
Comment on lines
99
to
102
| lemma mk_zero_eq_zero : (mk (0 : Fin size)) = (0 : $typeName) := by | ||
| delta OfNat.ofNat | ||
| delta $deltaName | ||
| simp only [ofNat, instOfNat, Zero.zero] |
There was a problem hiding this comment.
Suggested change
| lemma mk_zero_eq_zero : (mk (0 : Fin size)) = (0 : $typeName) := by | |
| delta OfNat.ofNat | |
| delta $deltaName | |
| simp only [ofNat, instOfNat, Zero.zero] | |
| lemma mk_zero_eq_zero : (mk (0 : Fin size)) = (0 : $typeName) := rfl |
Same here.
|
0307ddd implements |
Inline more items to Ring/CommRing, change some names for consistency.
|
bors merge |
bors bot
pushed a commit
that referenced
this pull request
Nov 19, 2021
Add new Fin instances, extend the UInt declarations to other UInt types using a macro. This incorporates @gebner's suggestions to add boolean methods for checking under/overflow, and adding separate instances of `Fin size`. I still can't figure out the elaboration issue mentioned [here on zulip](https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/simp.20type.20annotations/near/260877092), so I can't use the macro on USize yet.
|
Pull request successfully merged into master. Build succeeded: |
bors
bot
changed the title
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
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.
Add new Fin instances, extend the UInt declarations to other UInt types using a macro. This incorporates @gebner's suggestions to add boolean methods for checking under/overflow, and adding separate instances of
Fin size. I still can't figure out the elaboration issue mentioned here on zulip, so I can't use the macro on USize yet.