getI

Mathlib.Data.List.Defs

URI: https://scilib.ai/kg/mathlib#List.getI

Lean4

/-- "Inhabited" `get` function: returns `default` instead of `none` in the case
  that the index is out of bounds. -/
def getI [Inhabited α] (l : List α) (n : Nat) : α :=
  getD l n default

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

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

Разделы

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

Аффилиация

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