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

[Andrés Sicard-Ramírez]

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


-- 
Andrés
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.chalmers.se/pipermail/agda/attachments/20140203/d5ad6bc5/attachment.html