How to declare a finmap

Stream: new members

[Marcus Rossel]

I'm struggling with the definition of docs#finmap. It's defined as structure finmap {α : Type u} (β : α → Type v) : Type (max u v). Hence if I want a finmap with keys of type A and values of type B I have to write @finmap A (λ _, B). There must be a more elegant way. What am I missing?

Perhaps for context: I want to use finmap A B like dictionaries/hash-map would be in "regular" programming languages. I hope this is the correct type for that.

[Eric Wieser]

finmap (λ _ : A, B)

[Eric Wieser]

The reason this API feels weird to you is you're not using the more powerful dependently-typed cases, like x : finmap fin where x.lookup 2 : option (fin 2) etc.

[Marcus Rossel]

Yeah, I guess I'm just used to Lean providing a dependent and non-dependent version of these kinds of types ¯\_(ツ)_/¯