Documentation

Qq.ForLean.ToExpr

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