list simp lemmas?

Stream: new members

[Ben Selfridge]

In the VSCode extension, how do I list all lemmas currently tagged with the simp attribute?

[Isak Colboubrani]

Not in VS Code, but from the shell I think you should get (almost) all theorems/lemmas tagged with simp/simps using the following:

% git grep -A1 '@\[.*simp[^\]]*\]' Mathlib/ | grep 'theorem ' | wc -l
    2558
% git grep -A1 '@\[.*simp[^\]]*\]' Mathlib/ | grep 'lemma ' | wc -l
    1340

[Aaron Liu]

All simp theorems

import Lean

run_meta do
  let thms ← Lean.Meta.getSimpTheorems
  Lean.logInfo <| (thms.lemmaNames.toList.filterMap (fun x ↦ if let .decl name _ _ := x then some name else none)).map Lean.MessageData.ofConstName

[Aaron Liu]

(prone to stack overflow)

[Aaron Liu]

This version is less prone to stack overflow

import Mathlib

run_meta do
  let startPos := 0
  let endPos := 1024
  let thms ← Lean.Meta.getSimpTheorems
  let array := thms.lemmaNames.set.toArray
  Lean.logInfo m!"size : {array.size}"
  let mut res := m!""
  for i in array[startPos : endPos] do
    if let .decl name _ _ := i.fst then
      res := m!"{res ++ .ofConstName name}\n"
  Lean.logInfo res

[Isak Colboubrani]

Nice!

size : 67380

My claim about "[…] (almost) all theorems/lemmas […]" for the shell exercise above has been disproven.