Documentation

Mathlib.Tactic.Coe

Additional coercion notation #

Defines notation for coercions.

  1. ↑ t is defined in core.
  2. (↑) is equivalent to the eta-reduction of (↑ ·)
  3. ⇑ t is a coercion to a function type.
  4. (⇑) is equivalent to the eta-reduction of (⇑ ·)
  5. ↥ t is a coercion to a type.
  6. (↥) is equivalent to the eta-reduction of (↥ ·)

Elaborator for the (↑), (⇑), and (↥) notations.

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

    Partially applied coercion. Equivalent to the η-reduction of (↑ ·)

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

      Partially applied function coercion. Equivalent to the η-reduction of (⇑ ·)

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

        Partially applied type coercion. Equivalent to the η-reduction of (↥ ·)

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