Simplify the Gospel postcondition of [InfiniteArray.make].

This commit is contained in:
François Pottier 2022-02-15 17:15:26 +01:00
parent 0dd8df6d08
commit fc33d84f6f
1 changed files with 2 additions and 1 deletions

View File

@ -23,7 +23,8 @@ type 'a t
val make: int -> 'a -> 'a t
(*@ a = make n x
requires 0 < n
ensures forall i. 0 <= i -> a.view(i) = x *)
ensures forall i. a.view(i) = x *)
(* ensures a.view = (fun i -> x) *)
(**[get a i] reads the value stored at index [i] in the infinite array [a]. **)
val get: 'a t -> int -> 'a