• baseless_discourse@mander.xyz
    link
    fedilink
    arrow-up
    3
    ·
    edit-2
    1 year ago

    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?