Naming of unfolding lemmas

[gallais]

In Data.List.Properties we have:

unfold-reverse : ∀ (x : A) xs → reverse (x ∷ xs) ≡ reverse xs ∷ʳ x

ʳ++-defn : ∀ (xs : List A) {ys} → xs ʳ++ ys ≡ reverse xs ++ ys

Both lemmas are filling the same essential role: explain a complex
function (for efficiency reasons) in terms of more basic building
blocks. I think they should follow the same naming scheme & am in
favour of the unfold-X pattern.

[MatthewDaggitt]

Okay so I agree unfold is nicer than defn 👍

But I think that definition of unfold-reverse shouldn't be called either variant, as it's not really unfolding reverse, it's instead talking about the interaction of reverse and ∷ and therefore should be called reverse-∷ according to our existing conventions.

In contrast ʳ++-defn really is just unfolding the definition of ʳ++ and so I'm happy with calling it unfold-ʳ++. Depending on how many existing lemmas there are, I might be tempted to argue for switching the order so calling those lemmas ʳ++-unfold instead to make it more searchable...