Skip to content

Commit

Permalink
fix formatting
Browse files Browse the repository at this point in the history
  • Loading branch information
HSMF committed Nov 28, 2024
1 parent cfe458b commit e1d7e9f
Showing 1 changed file with 1 addition and 1 deletion.
2 changes: 1 addition & 1 deletion byteslice/byteslice.gobra
Original file line number Diff line number Diff line change
Expand Up @@ -45,7 +45,7 @@ pure func View(ub []byte) (res seq[byte]) {
}

ghost
requires forall i int :: {&ub[i]} 0 <= i && i < len(ub) ==> acc(&ub[i], _)
requires forall i int :: { &ub[i] } 0 <= i && i < len(ub) ==> acc(&ub[i], _)
ensures len(res) == len(ub)
ensures forall i int :: { res[i] } 0 <= i && i < len(ub) ==> res[i] == ub[i]
decreases len(ub)
Expand Down

0 comments on commit e1d7e9f

Please sign in to comment.