-
Benedikt Becker authored
When defined as a `val function` the postcondition of the program function `make` is just `result = make n v`, referring to the logical function `make`. But the equality cannot be proven because array equality is not defined. To facilitate proofs about results of the program functions `make`, this commit separates the definitions of the logical function from the program function `make`, so that the postconditions of the program function `make` refer to the properties of the resulting arrey.
1bb0c818