chore: Documentation about array initialization #1661
Conversation
MikaelMayer
added
the
part: documentation
docs/DafnyRef/Types.md
Outdated
| @@ -2409,7 +2409,10 @@ A one-dimensional array of `n` `T` elements is created as follows: | |||
| a := new T[n]; | |||
| ``` | |||
| The initial values of the array elements are arbitrary values of type | |||
| `T`. | |||
| `T`. They can also be initialized with the array display syntax: | |||
There was a problem hiding this comment.
I don't see "array display syntax" defined anywhere in the manual, so I wouldn't introduce this name without defining it.
Consider changing this to They can be initialized using an ordered list of expressions enclosed in square brackets, similar to a sequence display expression. Here is an example:
I based the above on this existing piece from the manual, which reads "A sequence can be formed using a sequence display expression, which is a possibly empty, ordered list of expressions enclosed in square brackets."
docs/DafnyRef/Types.md
Outdated
| @@ -2409,7 +2409,7 @@ A one-dimensional array of `n` `T` elements is created as follows: | |||
| a := new T[n]; | |||
| ``` | |||
| The initial values of the array elements are arbitrary values of type | |||
| `T`. They can also be initialized with the array display syntax: | |||
| `T`. They can also be initialized using a sequence display expression, as follows: | |||
There was a problem hiding this comment.
I think this is incorrect, since a sequence display expression also has another forms (seq(3, x => x *2)), and this only has the bracket form.
docs/DafnyRef/Types.md
Outdated
| @@ -2409,7 +2409,7 @@ A one-dimensional array of `n` `T` elements is created as follows: | |||
| a := new T[n]; | |||
| ``` | |||
| The initial values of the array elements are arbitrary values of type | |||
| `T`. They can also be initialized using a sequence display expression, as follows: | |||
| `T`. They can also be initialized using a sequence display expression delimited by square brackets, as follows: | |||
There was a problem hiding this comment.
I think 'delimited by square brackets' implies that multiple elements are separated by square brackets, like 1 [] 2 [] 3. I'd use the term 'enclosed' here.
Maybe you can reply to the suggestion I made earlier? #1661 (comment) That way I can understand what you didn't like about that.
docs/DafnyRef/Types.md
Outdated
| @@ -2409,7 +2409,7 @@ A one-dimensional array of `n` `T` elements is created as follows: | |||
| a := new T[n]; | |||
| ``` | |||
| The initial values of the array elements are arbitrary values of type | |||
| `T`. They can also be initialized using a sequence display expression delimited by square brackets, as follows: | |||
| `T`. They can also be initialized using a sequence display expression enclosed in square brackets, as follows: | |||
There was a problem hiding this comment.
I would leave out the 'also', otherwise it's implying the previous sentence already mentioned a way of initializing the values. Also, "a sequence display expression enclosed in square brackets" to me reads like there's an entire sequence display expression in square brackets, even though such as expression already has square brackets.
I think referring to a sequence display expression is a little confusing, since it's not exactly the same as this, so I'd prefer an explicit description like "an ordered list of expressions enclosed in square brackets". If we want to mention "sequence display expression" then I'd like to indicate it's only similar.
This fixes #1660
Array initialization with values was not documented yet.