Unused PrefixTrie and NameTrie

Stream: lean4 dev

[Joachim Breitner]

The lean4 code has a PrefixTrie data structure, and a NameTrie data structure wrapping it, but it seems neither is actually used, nor has been since two years. I’m inclined to remove such unused code (it is likely in good shape, but who knows, so maybe better not ship it to all lean users, and it can be resurrected when needed). Is a PR (like https://github.com/leanprover/lean4/pull/2551) to do so welcome?

[Joachim Breitner]

@Mac Malone says he might use them, closing the PR for now. I might come back in a few months :-)

[Leonardo de Moura]

@Joachim Breitner Looking forward to it :)