Skip to content

Commit

Permalink
Add some release notes that were forgotten
Browse files Browse the repository at this point in the history
  • Loading branch information
keyboardDrummer committed Oct 10, 2024
1 parent 2c6b638 commit f637859
Show file tree
Hide file tree
Showing 2 changed files with 2 additions and 0 deletions.
1 change: 1 addition & 0 deletions docs/dev/news/5761.feat
Original file line number Diff line number Diff line change
@@ -0,0 +1 @@
Added opaque blocks to the language. Opaque blocks enable improving verification performance. See the documentation for more details.
1 change: 1 addition & 0 deletions docs/dev/news/5779.feat
Original file line number Diff line number Diff line change
@@ -0,0 +1 @@
By blocks ("... by { ... }") are now available for assert statements, call statements, and the three types of assignments (:=, :-, :|). Also, by blocks should now be more intuitive since they enable proving any assertions on the left-hand side of the 'by', not just the 'outermost' one. For example, previously `assert 3 / x == 1 by { assume x == 3; }` could still give a possible division by zero error, but now it won't.

0 comments on commit f637859

Please sign in to comment.