I haven't read the tutorial at all, but in dependently typed languages the type (Fin N) is exactly the type of "natural numbers under N", and I expect that is what Edwin is using in the tutorial.

As for compiling to that pointer access: from what I know of Idris, yes it will. Since you know statically that the array access cannot be out of bounds, you can omit the usual out-of-bounds checks.