mk_natCast_nonneg_prf

Mathlib.Tactic.Linarith.Preprocessing

URI: https://scilib.ai/kg/mathlib#Mathlib.Tactic.Linarith.mk_natCast_nonneg_prf

Lean4

/-- If `e : ℕ`, returns a proof of `0 ≤ (e : C)`. -/
def mk_natCast_nonneg_prf (p : Expr × Expr) : MetaM (Option Expr) :=
  match p with
  | ⟨e, target⟩ =>
    try
      commitIfNoEx (mkAppM ``natCast_nonneg #[target, e])
    catch e =>
      do
        trace[linarith]"Got exception when using cast {e.toMessageData}"
        return none

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

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

Разделы

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

Аффилиация

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