Zulip Chat Archive

Stream: general

Topic: Finite maps


view this post on Zulip Ben Sherman (Nov 06 2018 at 20:17):

Is there a Lean (3) library for finite maps (i.e., key-value maps where finitely many keys are mapped to values)? I don't need performance, just reasoning really. But I'd also be fine if the key type requires decidable ordering (I would assume it would require at least decidable equality). Should I use this https://github.com/spl/lean-finmap?

view this post on Zulip Reid Barton (Nov 06 2018 at 20:21):

There's data.rbmap in the Lean standard library, does that meet your needs?

view this post on Zulip Mario Carneiro (Nov 06 2018 at 20:23):

There is also the finmap branch of leanprover-community which is porting Sean's work to mathlib

view this post on Zulip Mario Carneiro (Nov 06 2018 at 20:23):

and hash_map is also a finite map type

view this post on Zulip Mario Carneiro (Nov 06 2018 at 20:25):

on the non-computational side, finsupp is basically the type of finite maps (mapping everything out of domain to 0)

view this post on Zulip Ben Sherman (Nov 06 2018 at 20:30):

I'm looking for something that has unions and theorems about them. In this regard, both data.rbmap and data.hash_map are incomplete. And I do want to write programs, so finsupp is not what I'm looking for either. So it sounds like finmap is the way to go! Thanks for pointing me to the finmap branch of mathlib - I guess I'll use that. Thanks for the pointers, everyone!

view this post on Zulip Mario Carneiro (Nov 06 2018 at 20:37):

Ah, that's good to know. I'll work on adding unions to rbmap and hash_map


Last updated: May 14 2021 at 04:22 UTC