Mercurial > hg > Members > kono > Proof > galois

changeset 254:a5b3061f15ee

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
sym5n
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Tue, 15 Dec 2020 08:50:32 +0900
parents b46a3a3f45af
children 6d1619d9f880
files README.md sym5n.agda
diffstat 2 files changed, 6 insertions(+), 10 deletions(-) [+]
line wrap: on
line diff
--- 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
 
 ```
 
--- 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