succ'

Mathlib.Data.Num.Basic

URI: https://scilib.ai/kg/mathlib#Num.succ'

Lean4

/-- The successor of a `Num` as a `PosNum`. -/
def succ' : Num → PosNum
  | 0 => 1
  | pos p => succ p

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

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

Разделы

Аффилиация

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