[dllthomas]

It is! That's what is so cool about it! Idris lets you write an append that will work for any X and Y chosen at runtime, but will check that the result must have length X + Y at compile time.