Documentation

Qq.ForLean.ToExpr

source
@[implicit_reducible]
instance instToExprMVarId_qq :
Lean.ToExpr Lean.MVarId
source
@[implicit_reducible]
instance instToExprLevelMVarId_qq :
Lean.ToExpr Lean.LevelMVarId
source
def toExprLevel :
Lean.Level → Lean.Expr
Instances For
    source
    @[implicit_reducible]
    instance instToExprLevel_qq :
    Lean.ToExpr Lean.Level
    source
    @[implicit_reducible]
    instance instToExprBinderInfo_qq :
    Lean.ToExpr Lean.BinderInfo
    source
    @[implicit_reducible]
    instance instToExprMData_qq :
    Lean.ToExpr Lean.MData
    source
    def toExprExpr :
    Lean.Expr → Lean.Expr
    Instances For
      source
      @[implicit_reducible]
      instance instToExprExpr_qq :
      Lean.ToExpr Lean.Expr