Documentation

Qq.ForLean.ToExpr

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