The prospect of entering the remaining refinements one by one, by first focussing on their name and then using the editor, is rather forbidding. Luckily there is a possibility to avoid all the effort of focussing and retyping names: we can be guided by the Elan Programming Environment, so that we have to input only the bodies of the refinements.
We are focussed on the root and try to execute it.
Immediately we are warned of the fact that the first refinement is unknown.
We are now in backtrace-mood, and give the edit-command
The Elan Programming Environment responds by
After we enter the body, we return to the root of the program,
which we try to execute again.
In this way, we are made to enter one refinement at a time, until
the program is complete.
This guidance during input allows us to type most refinement names
only once, thus alleviating one of the drawbacks of Top-Down programming
and encouraging the use of meaningful identifiers.