walker (Aug 09 2022 at 21:07): 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.
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.
Gaëtan Gilbert (Aug 09 2022 at 21:14):how about fmapavl? https://github.com/coq/coq/blob/master/theories/FSets/FMapAVL.v
walker (Aug 09 2022 at 21:15):that is what I am looking for, thanks! (or I think so)
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: Oct 03 2023 at 04:02 UTC