Default value for external generic types #6049
Labels
kind: bug
Crashes, unsoundness, incorrect output, etc. If possible, add a `part:` label
lang: c++
Dafny's C++ transpiler and its runtime
part: code-generation
Support for transpiling Dafny to another language. If relevant, add a `lang:` tag
The C++ translator assumes there's a
get_XXXX_default()
for each external type.dafny/Source/DafnyCore/Backends/Cplusplus/CppCodeGenerator.cs
Line 1046 in e7e3ed4
While this works for non-generic types, for generic ones, even if such implementation exists, it still requires the generic (template) parameters to be passed to it.
For example:
The generated code will be:
If we provide a default function like below:
the C++ compiler does not infer
B
at the call site, and complains.The solution would be to provide
B
to the function call, or use the sameget_default
so the user specializes it for the external type.The text was updated successfully, but these errors were encountered: