rawCast

Mathlib.Tactic.NormNum.Result

URI: https://scilib.ai/kg/mathlib#Nat.rawCast

Lean4

/-- A "raw nat cast" is an expression of the form `(Nat.rawCast lit : α)` where `lit` is a raw
natural number literal. These expressions are used by tactics like `ring` to decrease the number
of typeclass arguments required in each use of a number literal at type `α`.
-/
@[simp]
def _root_.Nat.rawCast {α : Type u} [AddMonoidWithOne α] (n : ℕ) : α :=
  n

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

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

Разделы

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

Аффилиация

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