Defines notations for coercions.
↑ t↑ t
is defined in core.(↑)↑)
is equivalent to the eta-reduction of(↑ ·)↑ ·)
⇑ t⇑ t
is a coercion to a function type.(⇑)⇑)
is equivalent to the eta-reduction of(⇑ ·)⇑ ·)
↥ t↥ t
is a coercion to a type.(↥)↥)
is equivalent to the eta-reduction of(↥ ·)↥ ·)
def
Lean.Elab.Term.CoeImpl.elabPartiallyAppliedCoe
(sym : String)
(expectedType : Lean.Expr)
(mkCoe : Lean.Expr → 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.
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.