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 : Nat

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

instance Mathlib.Meta.FunProp.instInhabitedFunPropDecl : Inhabited FunPropDecl

Equations

• Mathlib.Meta.FunProp.instInhabitedFunPropDecl = { default := { funPropName := default, path := default, funArgId := default } }

instance Mathlib.Meta.FunProp.instBEqFunPropDecl : BEq FunPropDecl

Equations

• Mathlib.Meta.FunProp.instBEqFunPropDecl = { beq := Mathlib.Meta.FunProp.beqFunPropDecl✝ }

structure Mathlib.Meta.FunProp.FunPropDecls : Type

Discrimination tree for function properties.

• decls : Lean.Meta.DiscrTree FunPropDecl

  Discrimination tree for function properties.

instance Mathlib.Meta.FunProp.instInhabitedFunPropDecls : Inhabited FunPropDecls

Equations

• Mathlib.Meta.FunProp.instInhabitedFunPropDecls = { default := { decls := default } }

@[reducible, inline]

abbrev Mathlib.Meta.FunProp.FunPropDeclsExt : Type

Equations

• Mathlib.Meta.FunProp.FunPropDeclsExt = Lean.SimpleScopedEnvExtension Mathlib.Meta.FunProp.FunPropDecl Mathlib.Meta.FunProp.FunPropDecls

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.

Equations

• One or more equations did not get rendered due to their size.

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.

Equations

• One or more equations did not get rendered due to their size.

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

Is e a function property statement?

Equations

• Mathlib.Meta.FunProp.isFunProp e = do let __do_lift ← Mathlib.Meta.FunProp.getFunProp? e pure __do_lift.isSome

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

Equations

• Mathlib.Meta.FunProp.isFunPropGoal e = Lean.Meta.forallTelescope e fun (x : Array Lean.Expr) (b : Lean.Expr) => do let __do_lift ← Mathlib.Meta.FunProp.getFunProp? b pure __do_lift.isSome

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

Returns function property declaration from e = P f.

Equations

• Mathlib.Meta.FunProp.getFunPropDecl? e = do let __do_lift ← Mathlib.Meta.FunProp.getFunProp? e match __do_lift with | some (decl, snd) => pure (some decl) | none => pure none

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.

Equations

• Mathlib.Meta.FunProp.getFunPropFun? e = do let __do_lift ← Mathlib.Meta.FunProp.getFunProp? e match __do_lift with | some (fst, f) => pure (some f) | none => pure none

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

Turn tactic syntax into a discharger function.

Equations

• One or more equations did not get rendered due to their size.