chore: adaptations for nightly-2024-07-18#14888
Conversation
PR summary 0e4a3dc5dc
|
| File | Base Count | Head Count | Change |
|---|---|---|---|
| Mathlib.CategoryTheory.Category.Basic | 252 | 250 | -2 (-0.79%) |
| Mathlib.Algebra.Module.Equiv.Defs | 394 | 392 | -2 (-0.51%) |
| Mathlib.Testing.SlimCheck.Testable | 414 | 412 | -2 (-0.48%) |
| Mathlib.Tactic.Abel | 346 | 345 | -1 (-0.29%) |
| Mathlib.Computability.TuringMachine | 448 | 447 | -1 (-0.22%) |
| Mathlib.MeasureTheory.Constructions.Pi | 1228 | 1227 | -1 (-0.08%) |
| Mathlib.RingTheory.ClassGroup | 1228 | 1227 | -1 (-0.08%) |
| Mathlib.MeasureTheory.Function.SimpleFuncDenseLp | 1619 | 1618 | -1 (-0.06%) |
Import changes for all files
| Files | Import difference |
|---|---|
| Too many changes (4284)! |
Declarations diff
+ ext_iff'
+ instance : (forget V G).Faithful where map_injective w := Hom.ext w
+ instance [DecidableEq α] : DecidableEq αˣ := fun _ _ => decidable_of_iff' _ Units.ext_iff
+ mem_getLast?_append_of_mem_getLast?
+ mem_head?_append_of_mem_head?
- AddContent.ext_iff
- exists_eq_right'
- get!_none
- get!_some
- getLast?_append
- head?_append
- head_replicate
- instance : (forget V G).Faithful where map_injective w := Hom.ext _ _ w
- instance [DecidableEq α] : DecidableEq αˣ := fun _ _ => decidable_of_iff' _ ext_iff
- isSome_map
- takeWhile_cons_of_neg
- takeWhile_cons_of_pos
-+-+ Hom.ext'
------------------------------- ext_iff
You can run this locally as follows
## summary with just the declaration names:
./scripts/declarations_diff.sh <optional_commit>
## more verbose report:
./scripts/declarations_diff.sh long <optional_commit>|
✌️ semorrison can now approve this pull request. To approve and merge a pull request, simply reply with |
Co-authored-by: Johan Commelin <johan@commelin.net>
|
bors merge |
|
👎 Rejected by label |
|
bors merge |
|
Canceled. |
|
Ugh, let's just abandoned, it has been superseded by #14942 and It's not ideal, as we get a less granular history of updates for adaptations, but not terrible. |
No description provided.