Hi

Not sure of the best name for these kinds of sets but it’d be nice if there was a way of defining very trivial finite sets like {x, y, z} easily.

These sort of sets are useful for handling free variables. The free polynomial on two variables x, y N[{x, y}] is an example of the sort of thing I’m interested in. I’m really interested in figuring out variable binders and quantifiers in programming languages and I think this could be useful.

Not sure how to work with these kind of sets easily in Coq though.

From a theoretical perspective just using a nameless representation such as Fin from the vector package works but it’s kind of “icky” to work with directly. Also it just devolves into de Bruijn levels which I wanted to avoid.

Are there any packages for working with/declaring these kinds of sets?

Any advice?

IIRC you can use tactics to automate a little of this but I still don’t understand that sort of thing.

Ideally something like

```
Definition types: {x, y, z} -> typ := fun e =>
match e with
| x => pt
| y => exp N N
| z => N
end.
```

Would be possible but obvs that’s a lot to ask for