issue !4#5463: Review all names with `'`

Stream: triage

[Random Issue Bot]

Today I chose issue 5463 for discussion!

Review all names with '
Created by @Yury G. Kudryashov (@urkud) on 2023-06-24
Labels:

Is this issue still relevant? Any recent updates? Anyone making progress?

[Kim Morrison]

I commented on the issue with the list of all primed names (over 7000!) and the code to produce the list.

Presumably it will require a more targeted approach to make progress here.

[Kim Morrison]

I hope that we might aspire to one day not having primed names, but I'm not sure how we would ever get there.

[Yury G. Kudryashov]

How do I restrict the list to the definitions and lemmas defined in Mathlib, not its dependencies?

[Kim Morrison]

import Mathlib

open Lean

def primedNames : CoreM (Array Name) := do
  let env ← getEnv
  let mut r := #[]
  for (n, _) in env.constants.map₁.toList do
    if let some m := env.getModuleFor? n then
      if m.components.head! = `Mathlib then
        if n.toString.endsWith "'" then r := r.push n
  return r

run_meta do for n in ← primedNames do IO.println n

[Kim Morrison]

(Although arguably going via Environment.moduleData would be more efficient. For a small library like Mathlib the above code is no problem, however. :-)

[Yury G. Kudryashov]

Thank you!

[Random Issue Bot]

Today I chose issue 5463 for discussion!

Review all names with '
Created by @Yury G. Kudryashov (@urkud) on 2023-06-24
Labels:

Is this issue still relevant? Any recent updates? Anyone making progress?

[Violeta Hernández]

Relevant, but slowly getting better.