Skip to content

Commit

Permalink
Replace EmptySet with Empty (#8)
Browse files Browse the repository at this point in the history
Set in sets.EmptySet() is redundant; additionally, it will be more
consistent with the package for sequences (i.e., seqs.Empty())
  • Loading branch information
dnezam authored Nov 30, 2023
1 parent 7dfa81f commit a3bad3e
Showing 1 changed file with 5 additions and 5 deletions.
10 changes: 5 additions & 5 deletions sets/sets.gobra
Original file line number Diff line number Diff line change
Expand Up @@ -27,16 +27,16 @@ pure func IsEmpty(xs set[int]) bool {
ghost
ensures IsEmpty(result)
decreases
pure func EmptySet() (result set[int]) {
pure func Empty() (result set[int]) {
return set[int]{}
}

// There is only one empty set.
ghost
requires IsEmpty(xs)
ensures xs == EmptySet()
ensures xs == Empty()
decreases
pure func EmptySetIsUnique(xs set[int]) utils.Unit {
pure func EmptyIsUnique(xs set[int]) utils.Unit {
return utils.Unit{}
}

Expand Down Expand Up @@ -93,7 +93,7 @@ ensures forall i int :: { i in result } (a <= i && i < b) == i in result
ensures len(result) == b - a
decreases b - a
pure func Range(a, b int) (result set[int]) {
return a == b ? EmptySet() : Add(Range(a + 1, b), a)
return a == b ? Empty() : Add(Range(a + 1, b), a)
}

// Constructs a set with all integers in the range [0, n).
Expand Down Expand Up @@ -479,4 +479,4 @@ ensures len(xs) <= b - a
decreases
pure func BoundedSetLen(xs set[int], a, b int) utils.Unit {
return SubsetLen(xs, Range(a, b))
}
}

0 comments on commit a3bad3e

Please sign in to comment.