Make because a statement instead of expression

[raffopazzo]

Currently because is an expression. This allows to have fine-grained control of which subexpression needs which proof, for example f(x because A, y because B) but it complicates compiler internals. For example delta reduction needs to handle nonsensical situations like ({1,2,3} because true)[0]. An alternative approach is to allow an optional because clause at the statement level, for example in return x because y the clause is part of the return statement not the returned expression.

[raffopazzo]

For if statement it could be considered to support both

• if (cons) because x {...} where the reason x is visible in both branches (the curly braces might potentially be mandatory)
• if (cond because x) {...} where the reason x is visible only for the condition (the curly braces can remain optional for single-statement bodies)