Chapter 5: method factorial - do we need a return statement???

[CMAbramson]

Under the subheader: typical implementation of factorial function

I was wondering if you need to write "return f;" after you assign f := a; I know for Java you would need to write a return statement, but since Dafny does do many things differently, I wasn't sure if this was just simply a syntax difference.

[kevinsullivan]

Sorry for the delay responding to this issue. As you've inferred by now, no: all you need to do is assign the return value to the return parameter. You can optionally use a return statement.