[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