blob: 615ee2bc49e155df35ead915a1975a23981b7fe1 (
plain)
1
2
3
|
set-compr.dfy(25,7): Error: set comprehensions in non-ghost contexts must be compilable, but Dafny's heuristics can't figure out how to produce or compile a bounded set of values for 'o'
set-compr.dfy(51,13): Error: set comprehensions in non-ghost contexts must be compilable, but Dafny's heuristics can't figure out how to produce or compile a bounded set of values for 'o'
2 resolution/type errors detected in set-compr.dfy
|