Documentation

Qq.ForLean.ToExpr

source
instance instToExprMVarId_qq :
Lean.ToExpr Lean.MVarId
Equations
    source
    instance instToExprLevelMVarId_qq :
    Lean.ToExpr Lean.LevelMVarId
    Equations
      source
      instance instToExprFVarId_qq :
      Lean.ToExpr Lean.FVarId
      Equations
        source
        instance instToExprLevel_qq :
        Lean.ToExpr Lean.Level
        Equations
          source
          instance instToExprLiteral_qq :
          Lean.ToExpr Lean.Literal
          Equations
            source
            instance instToExprBinderInfo_qq :
            Lean.ToExpr Lean.BinderInfo
            Equations
              source
              instance instToExprMData_qq :
              Lean.ToExpr Lean.MData
              Equations
                source
                instance instToExprExpr_qq :
                Lean.ToExpr Lean.Expr
                Equations