# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1607989832 -32400
# Node ID a5b3061f15eed2446f6520bc6210d567db1d5881
# Parent  b46a3a3f45af8a2def1bfdfa33710594e5ef535a
sym5n

diff -r b46a3a3f45af -r a5b3061f15ee README.md
--- a/README.md	Sun Dec 13 17:31:00 2020 +0900
+++ b/README.md	Tue Dec 15 08:50:32 2020 +0900
@@ -27,6 +27,7 @@
 sym2n.agda           proved by Any
 sym3n.agda           
 sym4n.agda           
+sym5n.agda           command line computation for compile
 
 ```
 
diff -r b46a3a3f45af -r a5b3061f15ee sym5n.agda
--- a/sym5n.agda	Sun Dec 13 17:31:00 2020 +0900
+++ b/sym5n.agda	Tue Dec 15 08:50:32 2020 +0900
@@ -59,17 +59,12 @@
    FListtoStr [] = ""
    FListtoStr (cons a x x₁) = primStringAppend (FLtoStr a) (primStringAppend "\n" (FListtoStr x))
 
--- open import IO 
--- main = run ( putStrLn $ sym5solvable 4)
-
 open import Codata.Musical.Notation
 open import Data.Maybe hiding (_>>=_)
 open import Data.List  
 open import Data.Char  
--- open import Foreign.Haskell using (Unit)
 open import IO.Primitive
 open import Codata.Musical.Costring
--- open import Agda.Builtin.IO public
 
 postulate
     getArgs : IO (List (List Char))
@@ -96,13 +91,13 @@
 ... | just n = n
 ... | nothing  = 0
 
---main = run do
---  ♯ putStrLn "A string"
---  ♯ putStrLn "second string"
+
+--
+-- CommFListN 5 x is too slow use compiler
+-- agda --compile sym5n.agda
+--
 
 main : IO ⊤
 main = getArgs >>= (λ x →  putStrLn $ toCostring $ sym5solvable $ getNumArg1 x ) 
---    x <- getArgs
---    ? --♯ putStrLn $ toCostring $ sym5solvable $ getNumArg1 x