alist / finmap usage

Stream: new members

[Guilherme Espada]

In some proof I'm currently using a list of pairs as a map. (list (string × ttype))
However, I need uniqueness of keys, which isn't guaranteed by this approach. As such, I found alist and finmap.
My first question is: what is the difference between them?
My second question is, how do you instantiate the type? I expected the type to take two types (key, value), but it instead takes a function (?).
My third question is how you check if a specific key-value pair is in the map. In other words, how would you implement (def in_ctx (val: string × ttype) (ctx:list (string × ttype)) := val ∈ ctx)? I know there is a lookup operation, but I don't know how to handle the optional values.

Thanks

[Eric Wieser]

The function you want to pass is something like \lam _ : key_type, value_type

[Eric Wieser]

It's so you can have entries whose type depends on their key

[Guilherme Espada]

I implemented def in_ctx (key: string) (val: ttype) (ctx:ctxtype) := ctx.lookup key = (option.some val), does it look correct?