type

Mathlib.Tactic.FunProp.Theorems

URI: https://scilib.ai/kg/mathlib#Mathlib.Meta.FunProp.LambdaTheoremArgs.type

Lean4

/-- Convert `LambdaTheoremArgs` to `LambdaTheoremType`. -/
def type (t : LambdaTheoremArgs) : LambdaTheoremType :=
  match t with
  | .id => .id
  | .const => .const
  | .comp .. => .comp
  | .apply => .apply
  | .pi => .pi

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

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

Разделы

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

Аффилиация

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