dischargeQ?

Mathlib.Util.Simp

URI: https://scilib.ai/kg/mathlib#Lean.Meta.Simp.Methods.dischargeQ?

Lean4

/-- `Qq` version of `Lean.Meta.Simp.Methods.discharge?`, which avoids having to use `~q` matching
on the proof expression returned by `discharge?`

`dischargeQ? (a : Q(Prop))` attempts to prove `a` using the discharger, returning
`some (pf : Q(a))` if a proof is found and `none` otherwise. -/
@[inline]
def dischargeQ? (M : Methods) (a : Q(Prop)) : SimpM <| Option Q($a) :=
  M.discharge? a

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

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

Разделы

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

Аффилиация

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