Abstract import of concrete module is allowed, produces invalid target code #5854
Labels
invalid translated code
The compiler generates invalid code, making the the target language infrastructure crash
kind: bug
Crashes, unsoundness, incorrect output, etc. If possible, add a `part:` label
Dafny version
latest
Code to produce this issue
Command to run and resulting output
What happened?
The abstract import of a concrete module should be disallowed.
What type of operating system are you experiencing the problem on?
Mac
The text was updated successfully, but these errors were encountered: