Skip to content

Commit bb0ec0c

Browse files
chore(go): put back content() in mutable maps extern (#1694)
1 parent 49759c9 commit bb0ec0c

File tree

1 file changed

+9
-0
lines changed
  • StandardLibrary/runtimes/go/ImplementationFromDafny-go/DafnyLibraries

1 file changed

+9
-0
lines changed

StandardLibrary/runtimes/go/ImplementationFromDafny-go/DafnyLibraries/externs.go

Lines changed: 9 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -49,6 +49,15 @@ func (_this *MutableMap) Equals(other *MutableMap) bool {
4949
return _this == other
5050
}
5151

52+
// If you use the returned value, and ALSO continue to modify the MutableMap
53+
// Then things might get weird.
54+
func (_this *MutableMap) Content() _dafny.Map {
55+
if (_this.bytesKeys == true) {
56+
panic("To maintain compatibility with other runtimes, this method does not work when bytesKeys is true.");
57+
}
58+
return _this.dafnyInternal
59+
}
60+
5261
func (_this *MutableMap) EqualsGeneric(x interface{}) bool {
5362
other, ok := x.(*MutableMap)
5463
return ok && _this.Equals(other)

0 commit comments

Comments
 (0)