get

Mathlib.Tactic.FunProp.FunctionData

URI: https://scilib.ai/kg/mathlib#Mathlib.Meta.FunProp.MaybeFunctionData.get

Lean4

/-- Turn `MaybeFunctionData` to the function. -/
def get (fData : MaybeFunctionData) : MetaM Expr :=
  match fData with
  | .letE f | .lam f => pure f
  | .data d => d.toExpr

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

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

Разделы

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

Аффилиация

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