Lean4
/-- Register new function property. -/
def addFunPropDecl (declName : Name) : MetaM Unit := do
let info ← getConstInfo declName
let (xs, bi, b) ← forallMetaTelescope info.type
if ¬b.isProp then
throwError"invalid fun_prop declaration, has to be `Prop`-valued function"
let lvls := info.levelParams.map (fun l => Level.param l)
let e := mkAppN (.const declName lvls) xs
let path ← DiscrTree.mkPath e
let mut some funArgId ←
(xs.zip bi).findIdxM? fun (x, bi) => do
if (← inferType x).isForall && bi.isExplicit then
return true
else
return false |
throwError"invalid fun_prop declaration, can't find argument of type `α → β`"
let decl : FunPropDecl :=
{ funPropName := declName
path := path
funArgId := funArgId }
modifyEnv fun env => funPropDeclsExt.addEntry env decl
trace[Meta.Tactic.funProp.attr]"added new function property `{declName }`\nlook up pattern is `{path}`"
