fin (m+1) -> fin (n+1)

Stream: general

[Johan Commelin]

What is a good name for the function that sends i : fin (m+1) to i : fin (n+1) if i < n + 1 and to n : fin (n + 1) otherwise?
There is docs#fin.clamp which seems somewhat related, but that is a map nat -> fin (n + 1).

[Eric Wieser]

fin.clamp_fin? Is your proposed function different to calling clamp on a coercion?

[Johan Commelin]

No, I guess it is clamp after the coe from fin to nat.