# Provide a total version of `!!` for finite maps and lists

In case the type is inhabited, we can define a total version of the `lookup`

function as follows:

`l !!! i = match l !! i with Some x => x | None => inhabitant end`

Having such a total lookup function is often convenient. It came up in some discussions with Arthur and also @dfrumin requested having such a feature recently.

I would like to implement this by defining a type class `LookupTotal`

with its own notation (suggestion `!!!`

) and then have instances and lemmas for all of the usual data structures like maps and lists. For maps, we can define an instance like the above. For lists I would like to have an instance that is not just `m !!! i = if m !! i is Some x then x else inhabitant`

but something that is defined by structural recursion, so you can use it more easily in induction proofs.

We could furthermore provide an instance `LookupTotal (vec A n) (fin n) A`

for vectors. This operation is always total, regardless of whether `A`

is inhabited. Note that we already use the notation `!!!`

for vectors, so generalizing it to the type class based version as proposed here makes sense.