Skip to content

Commit

Permalink
add +gobra headers in all packages (#22)
Browse files Browse the repository at this point in the history
Adds a //+gobra comment to every package to ensure usability with the
`--onlyFilesWithHeader` flag
  • Loading branch information
HSMF authored Nov 28, 2024
1 parent 44af370 commit 7810723
Show file tree
Hide file tree
Showing 6 changed files with 7 additions and 1 deletion.
1 change: 1 addition & 0 deletions dicts/dicts.gobra
Original file line number Diff line number Diff line change
Expand Up @@ -13,6 +13,7 @@
- https://www.why3.org/stdlib/fmap.html
- https://www.why3.org/stdlib/map.html
*/
//+gobra

// This package defines lemmas for mathematical maps (aka dictionaries) commonly used
// in specifications.
Expand Down
1 change: 1 addition & 0 deletions gomap/gomap.gobra
Original file line number Diff line number Diff line change
Expand Up @@ -3,6 +3,7 @@
See LICENSE or go to https://github.com/viperproject/gobra-libs/blob/main/LICENSE
for full license details.
*/
//+gobra

// This package defines Go maps and their associated operations in terms of
// mathematical maps (dictionaries).
Expand Down
1 change: 1 addition & 0 deletions math/math.gobra
Original file line number Diff line number Diff line change
@@ -1,3 +1,4 @@
//+gobra
// This package defines mathematical operations commonly used in specifications.
package math

Expand Down
1 change: 1 addition & 0 deletions seqs/seqs.gobra
Original file line number Diff line number Diff line change
Expand Up @@ -6,6 +6,7 @@
This file is inspired by the standard libraries and axiomatisations of the following verifiers:
- dafny-lang/libraries: https://github.com/dafny-lang/libraries/blob/master/src/Collections/Sequences/Seq.dfy
*/
//+gobra

// This package defines lemmas for sequences commonly used in specifications.
package seqs
Expand Down
1 change: 1 addition & 0 deletions sets/sets.gobra
Original file line number Diff line number Diff line change
Expand Up @@ -10,6 +10,7 @@
- viperproject/silicon: https://github.com/viperproject/silicon/blob/master/src/main/resources/dafny_axioms/sets.vpr

*/
//+gobra

// This package defines lemmas for sets commonly used in specifications.
package sets
Expand Down
3 changes: 2 additions & 1 deletion util/util.gobra
Original file line number Diff line number Diff line change
Expand Up @@ -12,6 +12,7 @@
// See the License for the specific language governing permissions and
// limitations under the License.

//+gobra
package util

type Unit struct{}
Expand Down Expand Up @@ -50,4 +51,4 @@ requires b
decreases
pure func Asserting(ghost b bool) Unit {
return Unit{}
}
}

0 comments on commit 7810723

Please sign in to comment.