search

dafny-lang / libraries

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

forall statement with no bound variables is deprecated in `ModInternals` #130

Open seebees opened 1 year ago

seebees commented 1 year ago

Update ModInternals to use assert by

Example:

src/NonlinearArithmetic/Internals/ModInternals.dfy(94,4): Warning: a forall statement with no bound variables is deprecated; use an 'assert by' statement instead

MikaelMayer commented 1 year ago

I have tried a lot but there is something different with non-linear arithmetic that I don't know why but can't prove at all.