toRat

Mathlib.Tactic.NormNum.Result

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

Lean4

/-- Returns the rational number that is the result of `norm_num` evaluation. -/
def toRat {α : Q(Type u)} {e : Q($α)} : Result e → Option Rat
  | .isBool .. => none
  | .isNat _ lit _ => some lit.natLit!
  | .isNegNat _ lit _ => some (-lit.natLit!)
  | .isNNRat _ q .. => some q
  | .isNegNNRat _ q .. => some q

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

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

Разделы

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

Аффилиация

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