Result'

Mathlib.Tactic.NormNum.Result

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

Lean4

/-- The result of `norm_num` running on an expression `x` of type `α`.
Untyped version of `Result`. -/
inductive Result' where/-- Untyped version of `Result.isBool`. -/

  | isBool (val : Bool) (proof : Expr)/-- Untyped version of `Result.isNat`. -/

  | isNat (inst lit proof : Expr)/-- Untyped version of `Result.isNegNat`. -/

  | isNegNat (inst lit proof : Expr)/-- Untyped version of `Result.isNNRat`. -/

  | isNNRat (inst : Expr) (q : Rat) (n d proof : Expr)/-- Untyped version of `Result.isNegNNRat`. -/

  | isNegNNRat (inst : Expr) (q : Rat) (n d proof : Expr)
  deriving Inhabited

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

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

Разделы

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

Аффилиация

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