Currently when using if ... then ... else you often have to repeat code in the condition formula and in the then formula. This can be rather verbose and error-prone, e.g.:

if exists(getModule()) then result = getModule().getName()
else if isPublic() then result = "public"
else if ...

Trying to bind result in the condition formula would not work, because when the result is then also restricted somewhere else instead of having no result it would simply evaluate the else formula.

This could possibly be solved by introducing an if-then formula (feedback appreciated):
if-then(<variable-declarations> | <condition-formula> | <then-formula>) else <else-formula>

• <variable-declarations>: One or more variable declarations; zero declarations would probably make no sense since it would then be the same as a regular if ... then ... else formula
• <condition-formula>: If this formula holds, the <then-formula> is evaluated, otherwise the <else-formula> is evaluated

Example:

if-then(Module m |
 // Condition:
 m = getModule()
|
 // Then:
 result = m.getName()
)
else ...

Note that simple cases such as if ... then result = ... else result = ... could be solved using the defaults expression proposed by #5348; however the if-then formula proposed here would allow more complex scenarios such as chained if else formulas.