When you explain how expressions are substituted there are, I think, multiple mistakes. I've commented those on each line. (I had to format it as code to make it clear what I corrected ...)
====
This means whenever the Idris evaluator encounters
an expression of the form double x, with some expression
standing for x, it should be rewritten to x * 2. So, in the
example double (double 15):
Expression is now double (15 * 15) // 2 * 15
Expression is now double 30
Expression is now 30 * 30 // 2 * 30
First, the inner double 15 is rewritten to 15 * 15 // 2 * 15
15 * 15 is rewritten to 30 // 2 * 15
double 30 is rewritten to 30 * 30 // 2 * 30
30 * 30 is rewritten to 60 // 2 * 30
You might have noticed that instead of choosing to
evaluate the inner double 15 first, we could have
chosen the outer double (double 15), which would
have reduced to double 15 * double 15. Either order // (double 15) * 2
is possible, and each would lead to the same result.
Idris, by default, will evaluate the innermost expression
first. In other words, it will evaluate function arguments
before function definitions.
