catchNone

Mathlib.Tactic.Positivity.Core

URI: https://scilib.ai/kg/mathlib#Mathlib.Meta.Positivity.catchNone

Lean4

/-- Converts a `MetaM Strictness` which can fail
into one that never fails and returns `.none` instead. -/
def catchNone {e : Q($α)} (t : MetaM (Strictness zα pα e)) : MetaM (Strictness zα pα e) :=
  try
    t
  catch e =>
    trace[Tactic.positivity.failure]"{e.toMessageData}"
    pure .none

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

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

Разделы

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

Аффилиация

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