ofRawInt

Mathlib.Tactic.NormNum.Result

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

Lean4

/-- Constructs a `Result` out of a raw int cast.
Assumes `e` is a raw int cast expression denoting `n`. -/
def ofRawInt {α : Q(Type u)} (n : ℤ) (e : Q($α)) : Result e :=
  if 0 ≤ n then Result.ofRawNat e
  else
    Id.run do
      let .app (.app _ (rα : Q(Ring $α))) (.app _ (lit : Q(ℕ))) := e |
        panic! "not a raw int cast"
      .isNegNat rα lit (q(IsInt.of_raw $α (.negOfNat $lit)) : Expr)

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

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

Разделы

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

Аффилиация

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