Listing all identifiers

Stream: new members

[Isak Colboubrani]

What’s the recommended way to list all identifiers available (under the current imports)?

For example, with no imports I’d expect the list to include things like True.intro (constructor), rfl (definition), Nat(inductive type), Eq.trans (theorem), and so on. Once I add import Mathlib, it should also show entries such as npowBinRec.go_spec (a random Mathlib theorem), etc.

In other words, I want to enumerate everything I can successfully do #check <identifier> on.

[Aaron Liu]

You can list all "constants" pretty easily, by accessing the environment

[Aaron Liu]

Here's an example

import Lean

open Lean

run_meta do
  let env ← getEnv
  let consts := env.constants.toList

  -- to exclude compiler constants like `instMonadOption._cstage1`
  let safeConsts := consts.filter fun info => !info.snd.isUnsafe

  -- to exclude private definitions, like `_private.Lean.Meta.Basic.0.Lean.Meta.mkFreshExprMVarImpl`
  -- auxillary definitions, like `Init.PropLemmas._auxLemma.63`
  -- and internal definitions, like `Std.DTreeMap.Internal.Impl.get?`
  let safePublicConsts := safeConsts.filter fun info => !info.fst.isInternalOrNum


  logInfo m!"length : {safePublicConsts.length}"
  logInfo <| (safePublicConsts.map fun i => MessageData.ofConstName i.fst).take 50

[Aaron Liu]

This will not be a full list of all the things you can do #check <identifier> on, because some theorems are created on first use.

[Isak Colboubrani]

@Aaron Liu Thanks a lot. That is precisely what I was looking for!

[Isak Colboubrani]

With import Lean I get a list of 78,748 identifiers, and when adding import Mathlib I'm getting a total of 381,410 identifiers.

[Isak Colboubrani]

Importing Mathlib raises the identifier count by 302,662 (381,410 - 78,748). By comparison, the Mathlib statistics page reports a total of 309,920 entries—103,068 definitions and 206,852 theorems. A 2 % discrepancy feels quite reasonable given the applied filtering.