Simp theorems with type

Stream: lean4

[Marcus Rossel]

Is there some way to efficiently obtain all simp theorems whose equality matches a given type? So for example, simpThmsMatchingType (mkConst `Nat) would return all simp theorems of the form ∀ xs..., t₁ = t₂ where t₁ and t₂ are of type Nat.
I have very little understanding of how the discrimination tree for simp theorems works, so I'm not sure if this question even makes sense.

#xy

Perhaps it would also help to #xy here: I'm trying to pass an equality expression and a set of equational lemmas to an external equality saturation solver in hopes of it finding a sequence of rewrites that proves the equality. But as I don't want to pass all of Mathlib's 50000 simp lemmas, I'm trying to prune the set of lemmas first by keeping only those whose type even matches the equality. So, for example, if the goal equality is 2 * (x : Nat) = x + x, I don't want to provide simp theorems about Bool.

[Timo Carlin-Burns]

I don't think the discrimination tree structure provides much help here unless you know ahead of time all of the constants of type Nat. E.g. the LHS of a simp lemma fib 2 = 1 will be keyed by the path [.const `fib, .lit 2]