Rename `X_length` into `length_X`.

This follows https://github.com/coq/coq/pull/18564 This closes #213 (closed)

We didn't include our own copies of app_length and seq_length, but used those from the standard library. To make sure we can use them (without deprecation warnings) until support for Coq 8.19 is dropped, I included our own copies for the transition period. This was also suggested by @tchajed in #213 (closed).

Could you say how the MR was generated -- I presume everything outside list.v was auto-adjusted with the sed script?

No objection from my side, just some nits.

This seems great to me. It's a lot of churn in naming but this inconsistency has always bothered me; I use some of these lemmas so much (especially the lemma formerly known as app_length) it can be hard to remember what the standard convention even is.

added 1 commit

• a81164f7 - More comments.

Compare with previous version

LGTM, feel free to land with the comments tweaked and whenever you have the time to fix reverse dependencies.

added 1 commit

• d2df12d1 - More comments.

Compare with previous version

resolved all threads

merged

mentioned in commit 6190d85d

@iris-users This is a breaking change

• Rename lemmas X_length into length_X, see the sed script below for an overview. This follows https://github.com/coq/coq/pull/18564.