instance instToExprInt : Lean.ToExpr Int

Equations

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

instance instToExprMVarId : Lean.ToExpr Lean.MVarId

Equations

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

instance instToExprLevelMVarId : Lean.ToExpr Lean.LevelMVarId

Equations

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

instance instToExprFVarId : Lean.ToExpr Lean.FVarId

Equations

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

instance instToExprLevel : Lean.ToExpr Lean.Level

Equations

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

instance instToExprLiteral : Lean.ToExpr Lean.Literal

Equations

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

instance instToExprBinderInfo : Lean.ToExpr Lean.BinderInfo

Equations

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

instance instToExprMData : Lean.ToExpr Lean.MData

Equations

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

instance instToExprExpr : Lean.ToExpr Lean.Expr

Equations

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