The Coq mailing list

[Frédéric Besson <frederic.besson AT inria.fr>]

Hi,

I would consider the following options:
- AVL without proof terms (I think there is a Raw functor)
- Patricia Trees (I am at least aware of one implementation, ping  
alix.trieu AT cs.au.dk)
- Use native integers with the previous. 
In particular, Patricia trees show their full efficiency if the so-
called branching bit is computed in O(1).

Good luck,
--
Frédéric

On Wed, 2020-05-13 at 17:37 -0400, Gregory Malecha wrote:
> Hello --
> 
> I am wondering what people suggest as an efficient representation of
> finite maps. Normally I use positive maps but for this purpose I have
> a *very* sparse key space so it actually makes sense to store pairs
> of the key and the element. The standard library has an
> implementation of AVL trees, but the proof term that is store with
> data is prohibitively expensive. Are there other implementations of
> finite maps that the community can recommend?
> 
> Thanks.
>