filterOutImplementationDetails

Mathlib.Tactic.Core

URI: https://scilib.ai/kg/mathlib#Lean.Elab.Tactic.filterOutImplementationDetails

Lean4

/-- Given a local context and an array of `FVarIds` assumed to be in that local context, remove all
implementation details. -/
def filterOutImplementationDetails (lctx : LocalContext) (fvarIds : Array FVarId) : Array FVarId :=
  fvarIds.filter (fun fvar => !(lctx.fvarIdToDecl.find! fvar).isImplementationDetail)

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

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

Разделы

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

Аффилиация

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