inferLinearOrderedSemifield

Mathlib.Tactic.NormNum.Ineq

URI: https://scilib.ai/kg/mathlib#Mathlib.Meta.NormNum.inferLinearOrderedSemifield

Lean4

/-- Helper function to synthesize typed `Semifield α` `LinearOrder α` `IsStrictOrderedRing α`
expressions. -/
def inferLinearOrderedSemifield (α : Q(Type u)) :
    MetaM <| (_ : Q(Semifield $α)) × (_ : Q(LinearOrder $α)) × Q(IsStrictOrderedRing $α) :=
  let go := do
    let semifield ← synthInstanceQ q(Semifield $α)
    let linearOrder ← synthInstanceQ q(LinearOrder $α)
    let isStrictOrderedRing ← synthInstanceQ q(IsStrictOrderedRing $α)
    return ⟨semifield, linearOrder, isStrictOrderedRing⟩
  go <|> throwError"not a linear ordered semifield"

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

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

Разделы

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

Аффилиация

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