ReadOnly

Scoped array views supplied by NDArray.iterate. A view expires when its callback returns.

Imports

open Copy;

Table of Contents

Types

(type)

Scoped array views supplied by NDArray.iterate. A view expires when its callback returns.

type ReadOnly a

def read (_inst5313 : (Copy a)) (borrow xs : (ReadOnly a)) (i : Int | i ≥ 0 && i < size xs) : a

Functions declared as def f ... = uninterpreted: only their signature is known to the verifier; they have no body.

uninterpreted

def size : (xs : (ReadOnly a)) → Int