funProp environment extension that stores all registered function properties

structure Mathlib.Meta.FunProp.FunPropDecl : Type

Basic information about function property

To use funProp to prove a function property P : (α→β)→Prop one has to provide FunPropDecl.

• funPropName : Lean.Name

  function transformation name

• path : Array Lean.Meta.DiscrTree.Key

  path for discrimination tree

• funArgId : ℕ

  argument index of a function this function property talks about. For example, this would be 4 for @Continuous α β _ _ f

def Mathlib.Meta.FunProp.instInhabitedFunPropDecl.default : FunPropDecl

@[implicit_reducible]

instance Mathlib.Meta.FunProp.instInhabitedFunPropDecl : Inhabited FunPropDecl

def Mathlib.Meta.FunProp.instBEqFunPropDecl.beq : FunPropDecl → FunPropDecl → Bool

@[implicit_reducible]

instance Mathlib.Meta.FunProp.instBEqFunPropDecl : BEq FunPropDecl

structure Mathlib.Meta.FunProp.FunPropDecls : Type

Discrimination tree for function properties.

• decls : Lean.Meta.DiscrTree FunPropDecl

  Discrimination tree for function properties.

def Mathlib.Meta.FunProp.instInhabitedFunPropDecls.default : FunPropDecls

@[implicit_reducible]

instance Mathlib.Meta.FunProp.instInhabitedFunPropDecls : Inhabited FunPropDecls

@[reducible, inline]

abbrev Mathlib.Meta.FunProp.FunPropDeclsExt : Type

opaque Mathlib.Meta.FunProp.funPropDeclsExt : FunPropDeclsExt

Extension storing function properties tracked and used by the fun_prop attribute and tactic, including, for example, Continuous, Measurable, Differentiable, etc.

def Mathlib.Meta.FunProp.addFunPropDecl (declName : Lean.Name) : Lean.MetaM Unit

Register new function property.

def Mathlib.Meta.FunProp.getFunProp? (e : Lean.Expr) : Lean.MetaM (Option (FunPropDecl × Lean.Expr))

Is e a function property statement? If yes return function property declaration and the function it talks about.

def Mathlib.Meta.FunProp.isFunProp (e : Lean.Expr) : Lean.MetaM Bool

Is e a function property statement?

def Mathlib.Meta.FunProp.isFunPropGoal (e : Lean.Expr) : Lean.MetaM Bool

Is e a fun_prop goal? For example ∀ y z, Continuous fun x ↦ f x y z

def Mathlib.Meta.FunProp.getFunPropDecl? (e : Lean.Expr) : Lean.MetaM (Option FunPropDecl)

Returns function property declaration from e = P f.

def Mathlib.Meta.FunProp.getFunPropFun? (e : Lean.Expr) : Lean.MetaM (Option Lean.Expr)

Returns function f from e = P f and P is function property.

def Mathlib.Meta.FunProp.tacticToDischarge (tacticCode : Lean.TSyntax `tactic) : Lean.Expr → Lean.MetaM (Option Lean.Expr)

Turn tactic syntax into a discharger function.