What

Add inline array intialiser syntax to documentation

// This
var a := new int[] [1, 2, 3, 4];
// is better than
var a := new int[4];
a[0], a[1], a[2], a[3] := 1, 2, 3 , 4;

Why

This is an expected feature from the use in other languages such as c#. It should feel more obvious.

Background

I was trying to find a way to initialise an array to a list of values. I could not find this in the docs easily (cheatsheet, tutorial, quick reference). Except for doing it in spread assignment fashion.

I then found this PR which introduced the feature. However it seems it's undocumented:

72f60ac

Edit: I can see the syntax listed here:
https://dafny-lang.github.io/dafny/DafnyRef/DafnyRef#151-one-dimensional-arrays