I added these as a migration workaround for upgrading the Dafny version, but as a side effect this can make a class a mixed Dafny/native class when it wasn't intended to be, and this isn't supported on all target languages (e.g. Go). Easy fix to move them out of the class to the surrounding module instead.
Note that in this case InternalLegacyOverride was already a mixed class because of the policy constant, so a further refactoring will be necessary to support this in Go for e.g.
By submitting this pull request, I confirm that you can use, modify, copy, and redistribute this contribution, under the terms of your choice.
Description of changes:
I added these as a migration workaround for upgrading the Dafny version, but as a side effect this can make a class a mixed Dafny/native class when it wasn't intended to be, and this isn't supported on all target languages (e.g. Go). Easy fix to move them out of the class to the surrounding module instead.
Note that in this case
InternalLegacyOverridewas already a mixed class because of thepolicyconstant, so a further refactoring will be necessary to support this in Go for e.g.By submitting this pull request, I confirm that you can use, modify, copy, and redistribute this contribution, under the terms of your choice.