Commit d89c5df1 authored by POTTIER Francois's avatar POTTIER Francois
Browse files

Replaced [n >= 0] with [0 <= n].

parent d4fdebf2
......@@ -95,7 +95,7 @@ Hint Extern 1 (RegisterSpec Array_ml.set) => Provide set_spec.
Parameter make_spec :
curried 2%nat Array_ml.make /\
forall A n (x:A),
n >= 0 ->
0 <= n ->
app Array_ml.make [n x]
PRE \[]
POST (fun t => Hexists xs, t ~> Array xs \* \[xs = make n x]).
......@@ -189,7 +189,7 @@ Parameter sub_spec :
app Array_ml.sub [t ofs len]
INV (t ~> Array xs)
POST (fun t' => Hexists xs',
t' ~> Array xs'
t' ~> Array xs'
\* \[length xs' = len]
\* \[forall i, ofs <= i < len -> xs'[i] = xs[i]]).
......
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