getSortedAssertExists

Mathlib.Util.AssertExistsExt

URI: https://scilib.ai/kg/mathlib#Lean.Environment.getSortedAssertExists

Lean4

/-- `getSortedAssertExists env` returns the array of `AssertExists`, placing first all declarations,
in alphabetical order, and then all modules, also in alphabetical order. -/
def getSortedAssertExists (env : Environment) : Array AssertExists :=
  assertExistsExt.getState env |>.toArray.qsort fun d e =>
    (e.isDecl < d.isDecl) || (e.isDecl == d.isDecl && (d.givenName.toString < e.givenName.toString))

Похожие утверждения

Научная платформа российской исследовательской школы.

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru