Skip to content

Commit

Permalink
fix: Issue #2415 (#2419)
Browse files Browse the repository at this point in the history
* Edit per comment from Remy

* fix: Issue 2415

* Update docs/DafnyRef/Types.md

Co-authored-by: Mikaël Mayer <MikaelMayer@users.noreply.github.com>

* Adding text per comments

Co-authored-by: davidcok <davidcok@github.com>
Co-authored-by: Mikaël Mayer <MikaelMayer@users.noreply.github.com>
  • Loading branch information
3 people authored Jul 15, 2022
1 parent c584a2b commit 8792af1
Showing 1 changed file with 10 additions and 1 deletion.
11 changes: 10 additions & 1 deletion docs/DafnyRef/Types.md
Original file line number Diff line number Diff line change
Expand Up @@ -2805,8 +2805,17 @@ The initial values of the array elements are arbitrary values of type
```
a := new T[] [t1, t2, t3, t4];
```
The initial values can also be initialized using a lambda expressions, as follows:
```
a := new int[5](i => i*i);
```
In fact, the initializer can simply be a function name for the right type of function:
```
a := new int[5]{Square);
```

The length of an array is retrieved using the immutable `Length`
member. For example, the array allocated above satisfies:
member. For example, the array allocated with `a := new T[n];` satisfies:
```dafny
a.Length == n
```
Expand Down

0 comments on commit 8792af1

Please sign in to comment.