funProp tactic syntax

def Mathlib.Meta.FunProp.elabFunPropConfig : Lean.Syntax → Lean.Elab.Tactic.TacticM Config

fun_prop config elaborator

Equations

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

def Mathlib.Meta.FunProp.funPropTacStx : Lean.ParserDescr

Tactic to prove function properties

Equations

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

def Mathlib.Meta.FunProp.funPropTac : Lean.Elab.Tactic.Tactic

Tactic to prove function properties

Equations

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

def Mathlib.Meta.FunProp.«command#print_fun_prop_theorems__» : Lean.ParserDescr

Command that printins all function properties attached to a function.

For example

#print_fun_prop_theorems HAdd.hAdd

might print out

Continuous
  continuous_add, args: [4,5], priority: 1000
  continuous_add_left, args: [5], priority: 1000
  continuous_add_right, args [4], priority: 1000
  ...
Diferentiable
  Differentiable.add, args: [4,5], priority: 1000
  Differentiable.add_const, args: [4], priority: 1000
  Differentiable.const_add, args: [5], priority: 1000
  ...

You can also see only theorems about a concrete function property

#print_fun_prop_theorems HAdd.hAdd Continuous

Equations

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