added precondition n >= 0 to Array.make

parent c3d7c109
......@@ -43,7 +43,7 @@ module Array
| OutOfBounds -> { i < 0 \/ i >= length a }
val make (n: int) (v: 'a) :
{}
{ n >= 0 }
array 'a
{ result = {| length = n; elts = M.const v |} }
(* { length result = n /\ forall i:int. 0 <= i < n -> result[i] = v} *)
......
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