Documentation
Qq
.
ForLean
.
ToExpr
Search
Google site search
Qq
.
ForLean
.
ToExpr
source
Imports
Init
Lean
Imported by
instToExprInt
instToExprMVarId
instToExprLevelMVarId
instToExprFVarId
instToExprLevel
instToExprLiteral
instToExprBinderInfo
instToExprMData
instToExprExpr
source
instance
instToExprInt
:
Lean.ToExpr
Int
source
instance
instToExprMVarId
:
Lean.ToExpr
Lean.MVarId
source
instance
instToExprLevelMVarId
:
Lean.ToExpr
Lean.LevelMVarId
source
instance
instToExprFVarId
:
Lean.ToExpr
Lean.FVarId
source
instance
instToExprLevel
:
Lean.ToExpr
Lean.Level
source
instance
instToExprLiteral
:
Lean.ToExpr
Lean.Literal
source
instance
instToExprBinderInfo
:
Lean.ToExpr
Lean.BinderInfo
source
instance
instToExprMData
:
Lean.ToExpr
Lean.MData
source
instance
instToExprExpr
:
Lean.ToExpr
Lean.Expr