We use the ToExpr
type class to convert values of type α
into
expressions that denote these values in Lean.
Examples:
toExpr true = .const ``Bool.true []
toTypeExpr Bool = .const ``Bool []
See also ToLevel
for representing universe levels as Level
expressions.
- toExpr : α → Expr
Convert a value
a : α
into an expression that denotesa
- toTypeExpr : Expr
Expression representing the type
α