[Agda] C-c-C-n for NatShow.show n

[Sergei Meshveliani]

On Mon, 2014-02-03 at 09:00 -0500, Andrés Sicard-Ramírez wrote:
> 
> On 3 February 2014 08:43, Sergei Meshveliani <mechvel at botik.ru> wrote:
>         I have this minor question:
>         how to make the below code work under  C-c C-n  in  emacs
>         ?
>         
>         -----------------------------------------------
>         module Main where
>         open import Foreign.Haskell
>         open import IO.Primitive
>         open import Data.String as Str using (toCostring)
>         open import Data.Nat using (ℕ)
>         open import Data.Nat.Show as NatShow using ()
>         
>         n : ℕ
>         n = 203
>         
>         str = NatShow.show n
>         
>         main : IO Unit
>         main = putStrLn (toCostring str)
>         -------------------------------------------------
>         
>         
>         This is on  MAlonzo of January 26, 2014,  Debian Linux.
>         
>         I take this into  emacs,  command   C-c C-l
>                                             C-c C-n
>                                             str
>         
>         and expect to see the normalized value for  str   ("203").
> 
> 
> After a couple of minutes, I see "203".
> 


And it occurs that  n  is shown much faster than  str.

For example,  n = 80  is shown about 1000 times faster.
May be, 
       C-c C-n  
       n

does not call for  NatShow.show n
?

Regards,

------
Sergei