Commit 2021-01-20 16:12 7c892653
View on Github →chore(data/list/range): Add range_zero and rename range_concat to range_succ (#5821)
The name range_concat was derived from range'_concat, where there are multiple possible expansions for range' s n.succ.
For range there is only one choice, and naming the lemma after the result rather than the statement makes it harder to find.