Skip to content

Commit

Permalink
tests from Dionisios
Browse files Browse the repository at this point in the history
  • Loading branch information
jcp19 committed Oct 28, 2023
1 parent 8e9e0df commit 80450ec
Show file tree
Hide file tree
Showing 2 changed files with 30 additions and 0 deletions.
11 changes: 11 additions & 0 deletions src/test/resources/regressions/features/maps/maps-nested.gobra
Original file line number Diff line number Diff line change
@@ -0,0 +1,11 @@
// Any copyright is dedicated to the Public Domain.
// http://creativecommons.org/publicdomain/zero/1.0/

package pkg

ghost
func foo(){
mm := dict[int](dict[int]int){1 : {2:3}}
assert mm[1][2] == 3
assert 2 in domain(mm[1])
}
Original file line number Diff line number Diff line change
@@ -0,0 +1,19 @@
// Any copyright is dedicated to the Public Domain.
// http://creativecommons.org/publicdomain/zero/1.0/

package pkg

ghost
pure func bar(m dict[int]int, idx int) option[int] {
return idx in domain(m) ? some(m[idx]) : none[int]
}

ghost
pure func baz(m dict[int]int, idx int) option[int] {
return match idx in domain(m){
case true:
some(m[idx])
case false:
none[int]
}
}

0 comments on commit 80450ec

Please sign in to comment.