Further NameSet API

Stream: general

[Michael Rothgang]

In #20568, I'm using some further API for NameSets (an ofArray method); ImportGraph's [RequiredModules] file has some more API. I think this would fit well in a more central location.

batteries doesn't have anything about NameSet right now: would a PR adding this to core directly be welcome? CC @Kim Morrison

[Kim Morrison]

Please send it to Batteries first. It's had NameSet in the past, and can again. :-)

[Jon Eugster]

if you'd like to create a PR to ImportGraph after you've PRed some API to batteries, that would be very welcomed :)

[Michael Rothgang]

batterires#1091

[Yaël Dillies]

batteries#1091

[Michael Rothgang]

WIP PR at https://github.com/leanprover-community/import-graph/pull/49: help finishing it, after the batteries PR has been merged, is very welcome :-)