search

dafny-lang / dafny

Dafny is a verification-aware programming language
https://dafny.org
Other
2.9k stars 260 forks source link

Support for enumerating finite datatypes in Rust #5643

Closed fabiomadge closed 1 month ago

fabiomadge commented 2 months ago

Dafny version

4.7.0

Code to produce this issue

datatype D = A | B

const c := set d: D | true :: d

method Main() {
  print c, "\n";
}

Command to run and resulting output

No response

What happened?

EmitDatatypeBoundedPool unsupported

What type of operating system are you experiencing the problem on?

Mac

ssomayyajula commented 2 months ago

(documenting for anyone watching) workaround: declare c directly from the singleton constructors of D