Skip to content
Topazdocs
6.05.21

Search documentation

Specification 6.0

Use arrow keys to choose a result. Press Enter to open.

Type an API name, diagnostic number, rule, or project topic.

    Download →

    Library · Collections

    Array.get for T

    Return the element at an index, or None() for a negative index or one at or past the length.

    get(i: int) -> Option<T>
    Receiver
    Array<T>
    Minimum arity
    1
    Maximum arity
    1

    Declaration and parameters

    Availability

    Included by default · yes

    These types are provided by the language. No module import is required.

    The declarations below describe the standard operations on built-in values.

    Receiver

    Array<T>

    Parameter constraints

    Additional contracts are Pending.

    Array<T>.get(i: int) returns Option<T>. An index from zero to one less than the length returns Some with that element. A negative index or an index at or past the length returns None().

    get never faults for its index. Use values[i] when an index outside the array is a program error. That expression faults under the access rule.

    The length property returns the number of elements as int. An empty array has length 0.

    Array<T>.push(x: T) returns unit. It appends x after the last element and increases the length by one. Earlier elements keep their positions.

    Push writes to the array value. The receiver must be rooted in a let mut binding. Other array values are unchanged under collection value semantics.

    Related rule · Read, count and append array elements →

    Result

    Additional contracts are Pending.

    The declared result type is Option<T>.

    Effects

    Pending

    Failures

    Pending

    Result and effects

    The lookup never faults for its index. Index with values[i] when an index outside the array is a program error.

    Related entries

    Collections →

    Read, count and append array elements

    Ruletopaz.stdlib.contract.array-access-members.rule

    Read, count and append array elements

    Array<T>.get(i: int) returns Option<T>. An index from zero to one less than the length returns Some with that element. A negative index or an index at or past the length returns None().

    get never faults for its index. Use values[i] when an index outside the array is a program error. That expression faults under the access rule.

    The length property returns the number of elements as int. An empty array has length 0.

    Array<T>.push(x: T) returns unit. It appends x after the last element and increases the length by one. Earlier elements keep their positions.

    Push writes to the array value. The receiver must be rooted in a let mut binding. Other array values are unchanged under collection value semantics.

    Why

    A lookup that may miss returns its absence as a value, so reads of neighbors at the edges of a sequence need no separate bounds test. Indexing keeps its fault for indexes that a correct program never produces. The two intents keep two spellings. push builds a sequence in order without rebuilding it.

    Examples Read elements without faulting at the edges →Append elements to a mutable array →

    Read elements without faulting at the edges

    run · running · Verification · not-run

    main.tpzRead elements without faulting at the edgesOpen in Playground →
    1. import std.io
    3. let names = ["a", "b", "c"]
    4. for index in ([-1, 0, 2, 3]) {
    5. match (names.get(index)) {
    6. case Some(name) => io.writeLine("{index}: {name}")
    7. case None() => io.writeLine("{index}: none")
    8. }
    9. }
    10. let empty: Array<string> = []
    11. io.writeLine("{empty.length}: {empty.get(0) ?? "none"}")
    Expected outputExit code 0
    -1: none
0: a
2: c
3: none
0: none
    $ topaz run main.tpz · Target product 5.21.3
    Expected result

    Expected result

    Execution completes. Exit code 0.

    No stderr.

    Expected stdout
    1. -1: none
    2. 0: a
    3. 2: c
    4. 3: none
    5. 0: none

    This exact example has not been executed.

    Append elements to a mutable array

    run · running · Verification · not-run

    main.tpzAppend elements to a mutable arrayOpen in Playground →
    1. import std.io
    3. let mut names: Array<string> = []
    4. io.writeLine("{names.length}")
    5. names.push("a")
    6. names.push("b")
    7. io.writeLine("{names.length}: {names.join(",")}")
    Expected outputExit code 0
    0
2: a,b
    $ topaz run main.tpz · Target product 5.21.3
    Expected result

    Expected result

    Execution completes. Exit code 0.

    No stderr.

    Expected stdout
    1. 0
    2. 2: a,b

    This exact example has not been executed.

    Menu

    Download →