Zulip Chat Archive

Stream: mathlib4

Topic: Searching a DiscrTree


Moritz Doll (Dec 04 2022 at 09:13):

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 (Dec 05 2022 at 11:47):

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.


Last updated: Dec 20 2023 at 11:08 UTC