Zulip Chat Archive

Stream: general

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


Johan Commelin (Dec 28 2020 at 11:55):

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 (Dec 28 2020 at 12:24):

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

Johan Commelin (Dec 28 2020 at 12:47):

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


Last updated: Dec 20 2023 at 11:08 UTC