pushCore

Mathlib.Tactic.Push

URI: https://scilib.ai/kg/mathlib#Mathlib.Tactic.Push.pushCore

Lean4

/-- Common entry point to the implementation of `push`. -/
def pushCore (head : Head) (tgt : Expr) (disch? : Option Simp.Discharge) : MetaM Simp.Result := do
  let ctx : Simp.Context ← Simp.mkContext pushSimpConfig (simpTheorems := #[]) (congrTheorems := ← getSimpCongrTheorems)
  let methods :=
    match disch? with
    | none => { pre := pushStep head }
    | some disch => { pre := pushStep head, discharge? := disch, wellBehavedDischarge := false }
  (·.1) <$> Simp.main tgt ctx (methods := methods)

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

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

Разделы

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

Аффилиация

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