inhabited

Mathlib.Data.TypeVec

URI: https://scilib.ai/kg/mathlib#TypeVec.Curry.inhabited

Lean4

instance inhabited (F : TypeVec.{u} (n + 1) → Type*) (α : Type u) (β : TypeVec.{u} n) [I : Inhabited (F <| (β ::: α))] :
    Inhabited (Curry F α β) :=
  I

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

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

Разделы

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

Аффилиация

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