[Agda] Char + String

[Sergei Meshveliani]

Dear List,

I have the following simple question about Standard library.

To prepend  c : Char  to  str : String,  I write


   open import Data.String using (...) renaming (_++_ to _++'_)
   import Data.Char.Base as CharBase

   str' =  (CharBase.show c) ++' str



(++  is renamed, because there is also used  Data.List.++  in the
module).

Can this  str'  be written simpler?
For example, to prepend to Vec,  one can use  Data.Vec._∷_

Thanks,

------
Sergei