Skip to content

Commit

Permalink
Remove bad trigger
Browse files Browse the repository at this point in the history
Keeping this trigger causes profiling to fail, as the trigger cannot be found in the body of the quantifier.
  • Loading branch information
dnezam authored Mar 20, 2024
1 parent 0528eda commit 142d5d7
Showing 1 changed file with 1 addition and 1 deletion.
2 changes: 1 addition & 1 deletion dicts/dicts.gobra
Original file line number Diff line number Diff line change
Expand Up @@ -147,7 +147,7 @@ ghost
opaque
decreases
pure func IsTotal(d dict[int]int) bool {
return forall k int :: {d[k]} {k in domain(d)} k in domain(d)
return forall k int :: {k in domain(d)} k in domain(d)
}

// True iff a dictionary is monotonic.
Expand Down

0 comments on commit 142d5d7

Please sign in to comment.