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 (↥ ·)↥ ·)

ink

def Lean.Elab.Term.CoeImpl.elabPartiallyAppliedCoe (sym : String) (expectedType : Lean.Expr) (mkCoe : Lean.Expr → Lean.Expr → Lean.Elab.TermElabM Lean.Expr) : Lean.Elab.TermElabM Lean.Expr

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

Equations

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

ink

def Lean.Elab.Term.CoeImpl.«term(↑)» : Lean.ParserDescr

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

Equations

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

ink

def Lean.Elab.Term.CoeImpl.«term⇑_» : Lean.ParserDescr

⇑ t⇑ t coerces t to a function.

Equations

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

ink

def Lean.Elab.Term.CoeImpl.«term(⇑)» : Lean.ParserDescr

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

Equations

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

ink

def Lean.Elab.Term.CoeImpl.«term↥_» : Lean.ParserDescr

↥ t↥ t coerces t to a type.

Equations

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

ink

def Lean.Elab.Term.CoeImpl.«term(↥)» : Lean.ParserDescr

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

Equations

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