standard Map Types

Stream: new members

[Simon Daniel]

i was wondering if there is a built in type like Lean.AssocList where keys are unique. I know about HashMaps/RBMap, but those seem to more for performance optimizing.
if not would this be a sensible implementation?

def uniqueAssocList (a b: Type) [BEq a]:=
    {l: Lean.AssocList a b // ∀ (k:a), l.contains k -> ! (l.erase k).contains k}

[Ruben Van de Velde]

Hmm, I might have written it as something like "length of filter (equal to k) \le 1", but probably this works too

[Mario Carneiro]

docs#AList IIRC