Documentation

Mathlib.Tactic.FunProp.Elab

funProp tactic syntax #

fun_prop config elaborator

Equations
    Instances For

      Tactic to prove function properties

      Equations
        Instances For

          Tactic to prove function properties

          Equations
            Instances For

              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
                Instances For