Loops
"while" loops
Condition-bodied "while" loops
The condition and body can be combined.
This will repeatedly evaluate the body as long as it returns true.
Unlike the above example, this has an additional log of an empty option.
"until" loops
An until expression is like a while expression with the condition negated.
As with a while loop, the condition can be an option.
Since the condition is negated, the value is avaluable after the loop.
Condition-bodied "until" loops
As with a while loop, the condition and body can be combined.
The body can also return an option.
In that case, the value of the until expression is the first non-empty option returned by the body.
(It is unwrapped to a non-optional type, meaning nat instead of nat? below.)
This is the only kind of loop to not be void.