When inserting an expression before a decreases such as:
def foo(l: List[BigInt]): Unit = {
unfold(l)
decreases(l)
()
}
the console outputs :
[ Error ] Test.scala:8:5: Unexpected `decreases` (This error message might occur when a function has return type Unit while its body has another type).
decreases(l)
^^^^^^^^^^^^
[ Fatal ] Well-formedness check failed after extraction
This is not clear that the error comes from the fact that there was an expression other than a require before the decreases and in more involved cases the user tends to look at the return type of the body which is often what is not right when this specific error is returned.
When inserting an expression before a
decreases
such as:the console outputs :
This is not clear that the error comes from the fact that there was an expression other than a
require
before thedecreases
and in more involved cases the user tends to look at the return type of the body which is often what is not right when this specific error is returned.