search

dafny-lang / libraries

Libraries useful for Dafny programs
Other
43 stars 25 forks source link

The two Math.dfy files seem to cause problems #139

Open CarlKCarlK opened 10 months ago

CarlKCarlK commented 10 months ago

I notice there are two Math.dfy files. One in src and one in src/dafny

I'm using a new VS code, Dafny add-in install on Windows. When I try to compile src\Math.dfy (or src\Collections\Sequences\Seq.dfy) I get an error:

Dafny program verifier finished with 1 verified, 0 errors
Errors compiling program into library_example
(3009,40): error CS0234: The type or namespace name 'Abs' does not exist in the namespace 'Math' (are you missing an assembly reference?)

I can work around the error by renaming the module in src/Math.dfy to "Math2" and also changing the import in Seq.dfy.