Elan has a special mechanism for terminating the execution of a particular refinement, which looks like
This mechanism can in particular be used to terminate repetitions from the inside.
Although it looks much like the infamous goto-statement, the leave-statement is very different: It does not allow arbitrary continuation of program execution at some other part of the program with all its known dangers, but completes the execution of an algorithm. For this reason, you may name in a leave-statement only a refinement of whose execution the execution of the leave-statement is part. It is even possible to leave a refinement with a value, by
This causes the refinement with that name to be left, yielding the value of the expression.