Documentation

Mathlib.Tactic.FunProp.Decl

funProp environment extension that stores all registered function properties #

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 for discrimination tree

  • funArgId : Nat

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

Instances For

    Discrimination tree for function properties.

    Instances For
      @[reducible, inline]
      Equations
        Instances For

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

          Register new function property.

          Equations
            Instances For

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

              Equations
                Instances For

                  Is e a function property statement?

                  Equations
                    Instances For

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

                      Equations
                        Instances For

                          Returns function property declaration from e = P f.

                          Equations
                            Instances For

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

                              Equations
                                Instances For

                                  Turn tactic syntax into a discharger function.

                                  Equations
                                    Instances For