Noob meta question

Stream: general

[Chris Hughes]

What's the "correct" way to efficiently implement finitely supported functions in Lean meta. Currently I'm using list (α × β) as α →₀ β, but this seems totally wrong. By finitely supported, I mean functions for which I only care about the result for finitely many α

[Reid Barton]

data.rbmap?

[Reid Barton]

that's the best way I know of

[Sean Leather]

https://github.com/spl/lean-finmap ?

[Chris Hughes]

rbmap looks about right. Thanks.

[Chris Hughes]

Is there a decidable instance for mem in rbmap anywhere. This seems like something so fundamental that I feel like I must be doing something wrong by trying to use it.

[Sean Leather]

I don't think the rbmap theorem collection is very extensive.

[Chris Hughes]

I see there's contains, which I assume is the same thing.

[Chris Hughes]

There doesn't seem to be an erase either.

[Chris Hughes]

Is rbtree α isomorphic to finset α, and is rbmap α β isomorphic to Σ s : finset α, Π x, x ∈ s → β