Documentation

Mathlib.Tactic.Coe

Defines notations for coercions.

  1. ↑ t↑ t is defined in core.
  2. (↑)↑) is equivalent to the eta-reduction of (↑ ·)↑ ·)
  3. ⇑ t⇑ t is a coercion to a function type.
  4. (⇑)⇑) is equivalent to the eta-reduction of (⇑ ·)⇑ ·)
  5. ↥ t↥ 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.

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

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

⇑ t⇑ t coerces t to a function.

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

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

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

↥ t↥ t coerces t to a type.

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

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

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