ToExpr
instances for Mathlib #
instance
Mathlib.instToExprULiftOfToLevel_mathlib
{α✝ : Type s}
[Lean.ToExpr α✝]
[Lean.ToLevel]
[Lean.ToLevel]
:
Lean.ToExpr (ULift α✝)
Equations
Hand-written instance since PUnit
is a Sort
rather than a Type
.