MaybeFunctionData

Mathlib.Tactic.FunProp.FunctionData

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

Lean4

/-- Result of `getFunctionData?`. It returns function data if the function is in the form
`fun x => f y₁ ... yₙ`. Two other cases are `fun x => let y := ...` or `fun x y => ...` -/
inductive MaybeFunctionData where/-- Can't generate function data as function body has let binder. -/

  | letE (f : Expr)/-- Can't generate function data as function body has lambda binder. -/

  | lam (f : Expr)/-- Function data has been successfully generated. -/

  | data (fData : FunctionData)

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

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

Разделы

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

Аффилиация

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