The Coq mailing list

[Klaus Ostermann <klaus.ostermann AT uni-tuebingen.de>]

I have data that one would write down on a piece of paper as a table
with row and column headers.

The type of the headers is not "nat", though (otherwise I could use
nested vectors).
Let's call them R and C for the type of row headers and column headers,
respectively.
The type of the table elements is A.

Let's say I have finite sets r and c of R's and C's, respectively. r and
c are the labels
of a particular table.

Such a table should feature a function to look up an entry in the table,
which should
have a type similar to this:

lookup: Table R C r c A -> x in r -> y in c -> A

where "x in r" means a label x that is in the label set r.

In particular, the lookup function should not return an "option A".

Is there something like this in a standard library? How would I go about
this?

As a starter, is there something that is to standard finite maps as
vectors are to lists?
That is, finite maps where the type system keeps track of the available
keys?

Klaus