getFunProp? — Mathlib

Lean4
/-- Is `e` a function property statement? If yes return function property declaration and
the function it talks about. -/
def getFunProp? (e : Expr) : MetaM (Option (FunPropDecl × Expr)) := do
  let ext := funPropDeclsExt.getState (← getEnv)
  let decls ← ext.decls.getMatch e (← read)
  if h : decls.size = 0 then
    return none
  else
    if decls.size > 1 then
      throwError "fun_prop bug: expression {(← ppExpr e)} matches multiple function properties\n\
                  {decls.map (fun d => d.funPropName)}"
    let decl := decls[0]
    unless decl.funArgId < e.getAppNumArgs do
      return none
    let f := e.getArg! decl.funArgId
    return (decl, f)
Похожие утверждения