Skip to content

'in' -> 'elem' #52

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
jcp19 merged 1 commit into from
May 6, 2026
Merged

'in' -> 'elem' #52

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
2 changes: 1 addition & 1 deletion mode-gobra.js
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -71,7 +71,7 @@ ace.define(
var GobraHighlightRules = function () {
var gobra_keywords =
"invariant|requires|ensures|preserves|trusted|share|opaque|reveal|outline|pred|pure|exists|forall|assume|apply|inhale|exhale|assert|refute|ghost|implements|unfolding|let|fold|unfold|decreases|as|domain|axiom|adt|match|shared|exclusive|predicate|writePerm|noPerm|initEnsures|importRequires|proof|with|backend";
var gobra_operators = "==>|::|in|===|!==|@|--*|#|<!|!>"; // .. ?
var gobra_operators = "==>|::|in|elem|===|!==|@|--*|#|<!|!>"; // .. ?
var gobra_types = "seq|set|mset|dict|option|gpointer";
var gobra_functions = "acc|old|before|some|get|none|typeOf|isComparable";

Expand Down
2 changes: 1 addition & 1 deletion mode-golang.js
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -71,7 +71,7 @@ ace.define(
var GolangHighlightRules = function () {
var gobra_keywords =
"invariant|requires|ensures|preserves|trusted|share|opaque|reveal|outline|pred|pure|exists|forall|assume|apply|inhale|exhale|assert|refute|ghost|implements|unfolding|let|fold|unfold|decreases|as|domain|axiom|adt|match|shared|exclusive|predicate|writePerm|noPerm|initEnsures|importRequires|proof|with|backend";
var gobra_operators = "==>|::|in|===|!==|@|--*|#|<!|!>"; // .. ?
var gobra_operators = "==>|::|in|elem|===|!==|@|--*|#|<!|!>"; // .. ?
var gobra_types = "seq|set|mset|dict|option|gpointer";
var gobra_functions = "acc|old|before|some|get|none|typeOf|isComparable";

Expand Down
2 changes: 1 addition & 1 deletion src/02/maps.md
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -10,7 +10,7 @@ The accessibility predicate `acc(watched)` is for the entire map.
Individual elements, as in slices, are not addressable.

Holding write permissions, we can add entries.
In specifications, we can check with `in` if a key is contained in the map.
In specifications, we can check with `elem` if a key is contained in the map.
``` go verifies
watched["Blade Runner"] = true
// @ assert "Blade Runner" elem watched && len(watched) == 1
Expand Down
4 changes: 2 additions & 2 deletions src/mathematical-types.gobra
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -9,7 +9,7 @@ func sequences() {
// Constructing from a literal
s := seq[int]{0, 1, 1, 2, 3}
// Membership check
assert 1 in s && !(4 in s)
assert 1 elem s && !(4 elem s)
// Lookup
assert s[4] == 3
// Integer sequence shorthand
Expand Down Expand Up @@ -61,7 +61,7 @@ func sets() {
// Conversion from a set
s4 := set(s1)
// Membership
assert 1 in set[int]{1, 2} && !(0 in set[int]{1, 2})
assert 1 elem set[int]{1, 2} && !(0 elem set[int]{1, 2})
// Set operations
assert set[int]{0, 2} subset set[int]{0, 1, 2}
assert set[int]{0, 2} union set[int]{1} == set[int]{0, 1, 2}
Expand Down
8 changes: 4 additions & 4 deletions src/reference-mathematical-types.md
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -12,7 +12,7 @@ The type `seq[T]` represents finite sequences with elements of type `T`.
| `x ++ y` | `seq[T]` | `seq[T]` | `seq[T]` | concatenation |
| `x[i]` | `seq[T]` | | `T` | lookup the element at index `i` [^1] |
| `x == y` | `seq[T]` | `seq[T]` | `bool` | equality |
| `x in y` | `T` | `seq[T]` | `bool` | `true` if and only if `x` is an element of `y` |
| `x elem y` | `T` | `seq[T]` | `bool` | `true` if and only if `x` is an element of `y` |
| `seq[T]{}` | | | `seq[T]` | empty sequence |
| `seq[T]{x, y}` | `T` | `T` | `seq[T]` | literal[^2] |
| `seq[x..y]` | `I` | `I` | `seq[I]` [^3] | integer sequence \\( [x, x+1, \ldots, y-1] \\) |
Expand Down Expand Up @@ -52,7 +52,7 @@ The type `set[T]` represents [mathematical sets](https://en.wikipedia.org/wiki/S
| `x setminus y` | `set[T]` | `set[T]` | `set[T]` | \\( x \setminus y\\) |
| `x subset y` | `set[T]` | `set[T]` | `bool` | \\( x \subseteq y\\) |
| `x == y` | `set[T]` | `set[T]` | `bool` | \\( x = y\\) |
| `x in y` | `T` | `set[T]` | `bool` | \\( x \in y\\) |
| `x elem y` | `T` | `set[T]` | `bool` | \\( x \in y\\) |
| `len(x)` | `set[T]` | | `int` | \\( \|x\| \\) |
| `x # y` | `T` | `set[T]` | int | 1 if \\(x \in y\\) else 0 |
| `set(x)` | `set[T]` | | `set[T]` | conversion from a set |
Expand Down Expand Up @@ -85,7 +85,7 @@ The multiset operations respect the multiplicities of the elements.
| `x setminus y` | `mset[T]` | `mset[T]` | `mset[T]` |
| `x subset y` | `mset[T]` | `mset[T]` | `bool` |
| `x == y` | `mset[T]` | `mset[T]` | `bool` |
| `x in y` | `T` | `mset[T]` | `bool` |
| `x elem y` | `T` | `mset[T]` | `bool` |
| `len(x)` | `mset[T]` | | `int` |
| `x # y` | `T` | `mset[T]` | int | multiplicity of the element `x` in `y` |
| `mset(x)` | `mset[T]` | | `mset[T]` | conversion from a multiset |
Expand Down Expand Up @@ -121,7 +121,7 @@ The type `dict[K]V` represents dictionaries with keys of type `K` and values of
m1 := dict[string]int{ "one": 1, "two": 2, "one": -1}
^
```
[^6]: Requires `y in domain(x)`. Otherwise, an error is reported:
[^6]: Requires `y elem domain(x)`. Otherwise, an error is reported:
``` go
m1 := dict[string]int{ "one": 1, "two": 2}
assert m1["three"] == 3
Expand Down
Loading