/*
 * Copyright (c) 2020 Galois, Inc.
 * Distributed under the terms of the BSD3 license (see LICENSE file)
 */

module Array where

primitive type Array : * -> * -> *

primitive arrayConstant : {a, b} b -> (Array a b)
primitive arrayLookup : {a, b} (Array a b) -> a -> b
primitive arrayUpdate : {a, b} (Array a b) -> a -> b -> (Array a b)