Open robin-aws opened 1 week ago
I bumped into this while working on Mutations for the MPL. I think it is the Dafny code gen that does not support them, as compared to the runtimes.
I thought the Dafny codegen does support them, since it at least does the expected thing of generating method Foo()
instead of method Foo(input: Unit)
or whatever?
Inputs are fine.
Outputs are the problem.
i.e: the Dafny code generator wants something to put in returns
.
Having no input or output structure is a distinct case as well.