Commit 53e3cedd authored by Mário Pereira's avatar Mário Pereira

Array63: removed two unnecessary uses of [of_int] function

parent 13d586e6
......@@ -246,14 +246,14 @@ module Array63
ensures { 0 <= i < a.length }
ensures { result = a[i] }
raises { OutOfBounds -> i < 0 \/ i >= a.length }
= if i < of_int 0 || i >= length a then raise OutOfBounds;
= if i < 0 || i >= length a then raise OutOfBounds;
a[i]
let defensive_set (a: array 'a) (i: int63) (v: 'a)
ensures { 0 <= i < a.length }
ensures { a.elts = (old a.elts)[i <- v] }
raises { OutOfBounds -> (i < 0 \/ i >= a.length) /\ a = old a }
= if i < of_int 0 || i >= length a then raise OutOfBounds;
= if i < 0 || i >= length a then raise OutOfBounds;
a[i] <- v
val make (n: int63) (v: 'a) : array 'a
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment