[Agda] Char + String

[Sergei Meshveliani]

On Fri, 2017-05-05 at 23:25 +0300, Sergei Meshveliani wrote:
> 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) ?


I am sorry: may be this is

            Str.toString (c ∷ [])  ++' str

Regards,

------
Sergei