@[implicit_reducible]

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 [] }

@[implicit_reducible]

instance instToExprLevelMVarId_qq : Lean.ToExpr Lean.LevelMVarId

Equations

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

def toExprLevel : Lean.Level → Lean.Expr

Equations

• toExprLevel Lean.Level.zero = Lean.Expr.const `Lean.Level.zero []
• toExprLevel l.succ = Lean.mkApp (Lean.Expr.const `Lean.Level.succ []) (toExprLevel l)
• toExprLevel (l₁.max l₂) = Lean.mkApp2 (Lean.Expr.const `Lean.Level.max []) (toExprLevel l₁) (toExprLevel l₂)
• toExprLevel (l₁.imax l₂) = Lean.mkApp2 (Lean.Expr.const `Lean.Level.imax []) (toExprLevel l₁) (toExprLevel l₂)
• toExprLevel (Lean.Level.param n) = Lean.mkApp (Lean.Expr.const `Lean.Level.param []) (Lean.toExpr n)
• toExprLevel (Lean.Level.mvar n) = Lean.mkApp (Lean.Expr.const `Lean.Level.mvar []) (Lean.toExpr n)

@[implicit_reducible]

instance instToExprLevel_qq : Lean.ToExpr Lean.Level

Equations

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

@[implicit_reducible]

instance instToExprBinderInfo_qq : Lean.ToExpr Lean.BinderInfo

Equations

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

@[implicit_reducible]

instance instToExprMData_qq : Lean.ToExpr Lean.MData

Equations

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

def toExprExpr : Lean.Expr → Lean.Expr

Equations

• toExprExpr (Lean.Expr.bvar n) = Lean.mkApp (Lean.Expr.const `Lean.Expr.bvar []) (Lean.mkNatLit n)
• toExprExpr (Lean.Expr.fvar n) = Lean.mkApp (Lean.Expr.const `Lean.Expr.fvar []) (Lean.toExpr n)
• toExprExpr (Lean.Expr.mvar n) = Lean.mkApp (Lean.Expr.const `Lean.Expr.mvar []) (Lean.toExpr n)
• toExprExpr (Lean.Expr.sort l) = Lean.mkApp (Lean.Expr.const `Lean.Expr.sort []) (Lean.toExpr l)
• toExprExpr (Lean.Expr.const n ls) = Lean.mkApp2 (Lean.Expr.const `Lean.Expr.const []) (Lean.toExpr n) (Lean.toExpr ls)
• toExprExpr (f.app x_1) = Lean.mkApp2 (Lean.Expr.const `Lean.Expr.app []) (toExprExpr f) (toExprExpr x_1)
• toExprExpr (Lean.Expr.lam x_1 d b c) = Lean.mkApp4 (Lean.Expr.const `Lean.Expr.lam []) (Lean.toExpr x_1) (toExprExpr d) (toExprExpr b) (Lean.toExpr c)
• toExprExpr (Lean.Expr.forallE x_1 d b c) = Lean.mkApp4 (Lean.Expr.const `Lean.Expr.forallE []) (Lean.toExpr x_1) (toExprExpr d) (toExprExpr b) (Lean.toExpr c)
• toExprExpr (Lean.Expr.letE x_1 t v b c) = Lean.mkApp5 (Lean.Expr.const `Lean.Expr.letE []) (Lean.toExpr x_1) (toExprExpr t) (toExprExpr v) (toExprExpr b) (Lean.toExpr c)
• toExprExpr (Lean.Expr.lit l) = Lean.mkApp (Lean.Expr.const `Lean.Expr.lit []) (Lean.toExpr l)
• toExprExpr (Lean.Expr.mdata md e) = Lean.mkApp2 (Lean.Expr.const `Lean.Expr.mdata []) (Lean.toExpr md) (toExprExpr e)
• toExprExpr (Lean.Expr.proj s i e) = Lean.mkApp3 (Lean.Expr.const `Lean.Expr.proj []) (Lean.toExpr s) (Lean.mkNatLit i) (toExprExpr e)

@[implicit_reducible]

instance instToExprExpr_qq : Lean.ToExpr Lean.Expr

Equations

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