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

Sergei Meshveliani mechvel at botik.ru
Mon Feb 3 14:43:33 CET 2014


People,
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").
But it shows nothing, is silent.

1) For  str = "203",  it does show "203".
2) After  
          agda -c ... Main.agda
          ./Main

   done in the command line, it also prints  "203"  to the terminal.


Thanks,

------
Sergei



More information about the Agda mailing list