Convert `fin n` to `fin (n+1)`

Stream: new members

[Tage Johansson]

Hello,

Is there an easy way to convert a number of type fin n to fin (n+1). I tried library_search and got fin.succ but this obviously increases the number by one which is not what I want. I just want to cast/coerse/lift the number to a larger fin type.

I'd prefer a solution that looks very short and doesn't confuse the reader of the code. Something like ↑n or n.xxx.

Thanks,
Tage

[Andrew Yang]

docs#fin.cast_le should do.

[Damiano Testa]

In fact, both of the following work:

example (n : ℕ) (a : fin n) : fin (n+1) :=
fin.cast_le n.le_succ a

example (n : ℕ) (a : fin n) : fin (n+1) :=
fin.of_nat a

[Andrew Yang]

I'd advise for the former. The latter is actually a % succ n, which could cause problems later on.

[Reid Barton]

docs#fin.cast_succ