is this name used in mathlib

Stream: general

[Johan Commelin]

Is there some way to figure out whether with_zero.ordered_add_comm_monoid is used in mathlib?
(Of course I can delete the definition, build mathlib, and get an answer 2 hours later. But I'm looking for something a bit more responsive.)

[Johan Commelin]

Is this something that I could ask the olean files, in one way or another?

[Mario Carneiro]

If you have import all, you could scan all proof expressions for that constant

[Mario Carneiro]

you could also find the answer in the olean files

[Mario Carneiro]

import all

open tactic
run_cmd do
  env ← get_env,
  let l := env.fold mk_name_set $ λ d t,
    d.value.fold t (λ e _ t, match e with
      | expr.const n [] :=
        if n = `with_zero.ordered_add_comm_monoid then
          name_set.insert t d.to_name
        else t
      | _ := t
      end),
  tactic.trace l

[Johan Commelin]

Should this be a user command?

[Johan Commelin]

Or some script that we can run from scripts/ that will automatically setup the import all etc...

[Patrick Massot]

Give me a couple of 50 hours days and I'll get to that point of my TODO list (merge leancrawler and leanproject)

[Johan Commelin]

@Mario Carneiro Thanks! It seems that it isn't used.