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

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

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

Equations

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

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

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

Equations

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

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

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

Equations

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

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

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

Equations

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