Stream: Coq users

Topic: HashMap or equivalent impelementation?


view this post on Zulip walker (Aug 09 2022 at 21:07):

I am looking for data structure implementation or something that I can implement easily for Coq that provides extraction friendly/ search tree data structure that works with arbitrary keys. I assume I will have to implement equality function or hash functions for keys but I have no problem with that.

view this post on Zulip walker (Aug 09 2022 at 21:12):

If no such implementation exist, I am also welcoming papers on describing efficient implementation for functional programming languages, that I can just implement.

view this post on Zulip Gaƫtan Gilbert (Aug 09 2022 at 21:14):

how about fmapavl? https://github.com/coq/coq/blob/master/theories/FSets/FMapAVL.v

view this post on Zulip walker (Aug 09 2022 at 21:15):

that is what I am looking for, thanks! (or I think so)

view this post on Zulip Alexander Gryzlov (Aug 09 2022 at 22:40):

Search trees typically require total ordering on keys. I've recently ported a bunch of search structures from Isabelle to Coq/Ssreflect here: https://github.com/clayrat/fav-ssr


Last updated: Feb 09 2023 at 00:03 UTC