Zulip Chat Archive

Stream: general

Topic: best way to cast (i: fin n - 1)into (fin n)

Shi Zhengyu (Jan 05 2022 at 05:10):

Hi all,

I am wondering what is the best way to cast a (i: fin n - 1) into fin n for some natural number n.
with (ng1: n >= 1), (i: fin n - 1)I am currently using (fin.cast_lt i (lt_trans (fin.is_lt i) (buffer.lt_aux_2 ng1))). it works, but I am not sure it should be this complicated to do such simple task.


Shi Zhengyu (Jan 05 2022 at 05:15):


Mario Carneiro (Jan 05 2022 at 05:25):

docs#fin.cast_succ will cast fin n to fin (n+1), which is generally preferable (avoid subtraction)

Last updated: Dec 20 2023 at 11:08 UTC