Fin is a type of finite oridinals bounded by a nat. For example the WTF type in there is the same type as Fin 8.

Of course every language can have Fin with a fixed integer, like the post suggest, by just stacking options.

However for a properly defined Fin type, the input number is dynamic, serves as a bound for the element of the type. For example, Adga was able to type the fact that nth fibonacci number is a finite ordinal bounded by a function of n. Which I believe is not typable in rust?