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.