Documentation

Mathlib.Tactic.FunProp.Mor

funProp Meta programming functions like in Lean.Expr.* but for working with bundled morphisms. #

Function application in normal lean expression looks like .app f x but when we work with bundled morphism f it looks like .app (.app coe f) x where f. In mathlib coe is usually DFunLike.coe but it can be any coercion that is registered with the coe attribute.

The main difference when working with expression involving morphisms is that the notion the head of expression changes. For example in:

  coe (f a) b

the head of expression is considered to be f and not coe.

Is name a coerction from some function space to functions?

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

    Is e a coerction from some function space to functions?

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

      Morphism application

      Instances For

        Is e morphism application?

        Equations
        Instances For

          Weak normal head form of an expression involving morphism applications. Additionally, pred can specify which when to unfold definitions.

          For example calling this on coe (f a) b will put f in weak normal head form instead of coe.

          Weak normal head form of an expression involving morphism applications.

          For example calling this on coe (f a) b will put f in weak normal head form instead of coe.

          Equations
          Instances For

            Argument of morphism application that stores corresponding coercion if necessary

            Instances For

              Morphism application

              Equations
              Instances For

                Given e = f a₁ a₂ ... aₙ, returns k f #[a₁, ..., aₙ] where f can be bundled morphism.

                Equations
                Instances For

                  If the given expression is a sequence of morphism applications f a₁ .. aₙ, return f. Otherwise return the input expression.

                  Instances For

                    Given f a₁ a₂ ... aₙ, returns #[a₁, ..., aₙ] where f can be bundled morphism.

                    Equations
                    Instances For

                      mkAppN f #[a₀, ..., aₙ] ==> f a₀ a₁ .. aₙ where f can be bundled morphism.

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