chore: replace _aux with Aux in defs with no other underscores#40227
chore: replace _aux with Aux in defs with no other underscores#40227thorimur wants to merge 1 commit into
_aux with Aux in defs with no other underscores#40227Conversation
PR summary 65d0212d7bImport changes for modified filesNo significant changes to the import graph Import changes for all files
|
thorimur
temporarily deployed
to
cache-upload-forks
GitHub Actions
Inactive
grunweg
left a comment
grunweg
left a comment
There was a problem hiding this comment.
Thanks for doing this! My biggest comment is that some of these renames probably require deprecations. (If you want to make some of them private first, perhaps you can omit that step :-))
| There is some equivalence between `m` and `m.map f` which respects `f`. | ||
| -/ | ||
| def mapEquiv_aux (m : Multiset α) (f : α → β) : | ||
| def mapEquivAux (m : Multiset α) (f : α → β) : |
There was a problem hiding this comment.
Does this need a deprecation? (and/or a TODO to make private)
| we also have a value on the other side of the equivalence | ||
| -/ | ||
| def removeNone_aux (x : α) : β := | ||
| def removeNoneAux (x : α) : β := |
| theorem removeNone_aux_some {x : α} (h : ∃ x', e (some x) = some x') : | ||
| some (removeNone_aux e x) = e (some x) := by | ||
| simp [removeNone_aux, Option.isSome_iff_exists.mpr h] | ||
| theorem removeNoneAux_some {x : α} (h : ∃ x', e (some x) = some x') : |
| theorem removeNone_aux_none {x : α} (h : e (some x) = none) : | ||
| some (removeNone_aux e x) = e none := by | ||
| simp [removeNone_aux, Option.not_isSome_iff_eq_none.mpr h] | ||
| theorem removeNoneAux_none {x : α} (h : e (some x) = none) : |
| some (removeNoneAux e x) = e none := by | ||
| simp [removeNoneAux, Option.not_isSome_iff_eq_none.mpr h] | ||
|
|
||
| theorem removeNone_aux_inv (x : α) : removeNone_aux e.symm (removeNone_aux e x) = x := |
There was a problem hiding this comment.
and here... and this declaration is mis-named (pre-existing; leaving a TODO is fine with me)
| @@ -650,28 +650,28 @@ termination_by structural x => x | |||
| Generalization of `sModNat` with arbitrary base case, | |||
There was a problem hiding this comment.
Do the rename in the nolints file, then we're all happy :-)
| useful for proving `sModNatTR` and `sModNat` agree. | ||
| -/ | ||
| def sModNat_aux (b q : ℕ) : ℕ → ℕ | ||
| def sModNatAux (b q : ℕ) : ℕ → ℕ |
| This produces `2^n` branches when there are `n` such hypotheses in the input. | ||
| -/ | ||
| partial def removeNe_aux : MVarId → List Expr → MetaM (List Branch) := fun g hs => do | ||
| partial def removeNeAux : MVarId → List Expr → MetaM (List Branch) := fun g hs => do |
| | i + 1 => (sModNatAux b q i ^ 2 + (q - 2)) % q | ||
|
|
||
| theorem sModNat_aux_eq (q k : ℕ) : sModNat_aux (4 % q) q k = sModNat q k := by | ||
| theorem sModNatAux_eq (q k : ℕ) : sModNatAux (4 % q) q k = sModNat q k := by |
grunweg
added
awaiting-author
2 participants
Found by regex (
def [^_]*_aux), and hand-replaced to avoid false positives.Usually,
_auxdefs with more than one underscore are named after other out-of-convention defs, so we don't touch those cases here.(Some of these are private, but naming is also a source readability concern, not just a public API concern.)