IndexableMut

trait IndexableMut[t: Type] with Indexable[t]Source

An IndexableMut instance on a type means that it has a (potentially partial) mapping from indices (Indexable.Idx) to elements (Indexable.Elm). The mapping can be modified and potentially expanded. The mapping can be accessed by Indexable.get and modified by put.

If only a subset of indices are allowed to be modified (e.g. only a range of integers is valid) then then Aef should include an error like OutOfBounds or KeyNotFound.

An instance of IndexableMut requires an instance of Indexable where the type of indices and elements are defined. The associated effect here can be different from Indexable, because some data structures might allow all modifications (like Map) while only defining a subset of mappings.

It must hold that { IndexableMut.put(i, v, x); Indexable.get(i, x) } == v for all i, v, and x: t with IndexableMut[t] if it does not stop with an effect. Note that the get should not fail based on the key if put does not.

Associated Types

type Aef: EffSource

The effect of put.

Instances

instance IndexableMut[Array[a, r]]Source

instance IndexableMut[MutHashMap[k, v, r]] with Eq[k], Hash[k]Source

instance IndexableMut[MutList[a, r]]Source

instance IndexableMut[MutMap[k, v, r]] with Order[k]Source

Signatures

def put(t: t, i: Idx[t], v: Elm[t]): Unit \ Aef[t] with IndexableMut[t] Source

Insert the element v at index i in t, overriding the existing element if there is one.