throwNone

Mathlib.Tactic.Positivity.Core

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

Lean4

/-- Converts a `MetaM Strictness` which can return `.none`
into one which never returns `.none` but fails instead. -/
def throwNone {m : Type → Type*} {e : Q($α)} [Monad m] [Alternative m] (t : m (Strictness zα pα e)) :
    m (Strictness zα pα e) := do
  match ← t with
  | .none =>
    failure
  | r =>
    pure r

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

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

Разделы

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

Аффилиация

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