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

source
instance instToExprLevelMVarId_qq :
Lean.ToExpr Lean.LevelMVarId
Equations

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

source
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)

Instances For

source
instance instToExprLevel_qq :
Lean.ToExpr Lean.Level
Equations

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

source
instance instToExprBinderInfo_qq :
Lean.ToExpr Lean.BinderInfo
Equations

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

source
instance instToExprMData_qq :
Lean.ToExpr Lean.MData
Equations

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

source
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)

Instances For

source
instance instToExprExpr_qq :
Lean.ToExpr Lean.Expr
Equations

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