Searching a DiscrTree

Stream: mathlib4

[Moritz Doll]

I have a d : DiscrTree Name true and I want to know whether a given decl : Name is in that tree.
I've tried something

def foo (tree : DiscrTree Name true) (declName : Name) : CoreM Bool := MetaM.run' do
  match_list ← tree.getMatch (Lean.Expr.const declName [])
  return !match_list.isEmpty

but it does not seem to work and it feels wrong. Is there a simple way to do this? I did not find any case where the tree is searched, for the simpTheorems and Instances there is a separate hashmap that contains the lemma names, but Mathlib.Tactic.Relation.Symm (and also Refl) have only the tree.

[Jannis Limperg]

If you want to fold over the values in the DiscrTree, I have functions for this that I'll PR to std4 shortly. Otherwise the DiscrTree API is indeed a bit bare-bones, so your best bet may be to introduce auxiliary data structures like the hashmaps you mentioned.