[Agda] Char + String

[Sergei Meshveliani]

On Fri, 2017-05-05 at 13:25 +0300, Sergei Meshveliani wrote:
> [..]

> 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).


It occurs that this is not prepending a Char, because the above `show'
sets something extra there.

Instead it works
           Str.toString (c ∷ (Str.fromString str)).

It costs  O(length str). 

But is there possible a simpler expression
(and not so expensive) ?

Thanks,

------
Sergei