whnfQuantifier

Mathlib.Tactic.Peel

URI: https://scilib.ai/kg/mathlib#Mathlib.Tactic.Peel.whnfQuantifier

Lean4

/-- If `unfold` is false then do `whnfR`, otherwise unfold everything that's not a quantifier,
according to the `quantifiers` list. -/
def whnfQuantifier (p : Expr) (unfold : Bool) : MetaM Expr := do
  if unfold then
    whnfHeadPred p fun e => if let .const n .. := e.getAppFn then return !(n ∈ quantifiers) else return false
  else
    whnfR p

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

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

Разделы

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

Аффилиация

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