instance instToExprMVarId_qq : Lean.ToExpr Lean.MVarId

Equations

• instToExprMVarId_qq = { toExpr := fun (i : Lean.MVarId) => Lean.mkApp (Lean.Expr.const `Lean.MVarId.mk []) (Lean.toExpr i.name), toTypeExpr := Lean.Expr.const `Lean.MVarId [] }

instance instToExprLevelMVarId_qq : Lean.ToExpr Lean.LevelMVarId

Equations

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

instance instToExprFVarId_qq : Lean.ToExpr Lean.FVarId

Equations

• instToExprFVarId_qq = { toExpr := fun (i : Lean.FVarId) => Lean.mkApp (Lean.Expr.const `Lean.FVarId.mk []) (Lean.toExpr i.name), toTypeExpr := Lean.Expr.const `Lean.FVarId [] }

instance instToExprLevel_qq : Lean.ToExpr Lean.Level

Equations

• instToExprLevel_qq = { toExpr := toExprLevel✝, toTypeExpr := Lean.Expr.const `Lean.Level [] }

instance instToExprLiteral_qq : Lean.ToExpr Lean.Literal

Equations

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

instance instToExprBinderInfo_qq : Lean.ToExpr Lean.BinderInfo

Equations

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

instance instToExprMData_qq : Lean.ToExpr Lean.MData

Equations

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

instance instToExprExpr_qq : Lean.ToExpr Lean.Expr

Equations

• instToExprExpr_qq = { toExpr := toExprExpr✝, toTypeExpr := Lean.Expr.const `Lean.Expr [] }