mathport/align questions

Stream: mathlib4

[Arien Malec]

1. Do we manually #align things that mathport gets right, or no?
2. I've noticed that mathport is better about getting names right in signatures than in def bodies, which requires manual fixing for recursive calls.... -- might be a "won't fix"
3. There appears to be a feature in Lean 3 where I can default a constant parameter in a recursive call, and I can't in Lean 4 -- requires manual fixing.... -- not sure if it's feasible to address this in mathport?

e.g., in Lean 3, this works

protected def traverse {F : Type u → Type v} [applicative F] {α β : Type*} (f : α → F β) :
  list α → F (list β)
| [] := pure []
| (x :: xs) := list.cons <$> f x <*> traverse xs

Whereas in Lean 4, I need to explicitly include the f parameter:

protected def traverse
    {F : Type u → Type v}
    [Applicative F]
    {α β : Type _}
    (f : α → F β) : List α → F (List β)
  | [] => pure []
  | x :: xs => List.cons <$> f x <*> List.traverse f xs
#align list.traverse List.traverse

4. This one was just funny: I stared at a line that was let rec := <foo> in Lean 3 and Lean 4 for a long long time trying to figure out how it even worked in Lean 3, until I realized that let rec wasn't a thing in Lean 3 and rec was being parsed as a legal variable...

[Kevin Buzzard]

Re 1: recent mathlib3port efforts have been aligning everything and I've not been deleting stuff which it gets right!

[Scott Morrison]

Re: 2. mathport is trying as hard as it can. Getting names right is hard.

[Arien Malec]

Trust me that I understand that the fact that mathport works as well as it does is a celebration....

[Arien Malec]

migrations are the 3rd hardest problem in software engineering, behind naming things, cache invalidation and off-by-one errors