Commit 2025-01-06 14:48 15b2729d

feat(Combinatorics/SimpleGraph/Walk): add penultimate and snd (#16769) Here are some reasons for it:

• We want to add penultimate, as p.getVert (p.length - 1) duplicates p, and snd should exist for symmetry.
• In some cases it makes sense to consider the vertices of a walk without the first/last one, and then this is the walk version of List.head/List.last, not l[1]/l[l.size-2]
• In walks the first/last node and adjacency are a lot more important than they usually are in lists, so it makes more sense to have a special term for the node adjacent to the first/last node.
• Walks always have a sensible default, so there's no need for the "take a proof/default value/panic/return an option" duplication which lists have and so this doesn't require much API.