How can I find if a subexpression occurs in a lean theo...

Stream: metaprogramming / tactics

[AG]

I want to see if the "combinatorics.simple_graph.degree" shows up in any theorems.

The way I did it was:

meta def check_for_degree (e : expr) : tactic bool :=
do {
  degree_decl ←  tactic.get_decl ``degree,
  let degree_expr := degree_decl.type,
  return $ expr.occurs degree_expr e
}

But, Lean prints "false" in the working example here.

What should I change?

Any help would be much appreciated!

[Notification Bot]

AG has marked this topic as resolved.

[Notification Bot]

AG has marked this topic as unresolved.

[Eric Wieser]

Why are you looking for the type of the decl?

[Eric Wieser]

Does checking for `degree in docs#expr.list_constant do what you need?

[AG]

Oh yes that's perfect! Thank you very much. This gives back the desired result now:

let constants_in_e := e.list_constant,
let contains_degree := constants_in_e.contains ``degree,