ofRawNat

Mathlib.Tactic.NormNum.Result

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

Lean4

/-- Constructs a `Result` out of a raw nat cast. Assumes `e` is a raw nat cast expression. -/
def ofRawNat {α : Q(Type u)} (e : Q($α)) : Result e :=
  Id.run do
    let .app (.app _ (sα : Q(AddMonoidWithOne $α))) (lit : Q(ℕ)) := e |
      panic! "not a raw nat cast"
    .isNat sα lit (q(IsNat.of_raw $α $lit) : Expr)

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

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

Разделы

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

Аффилиация

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