Mercurial > hg > Members > kono > Proof > galois

changeset 292:f59a9f4cfd78

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
fix
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Sun, 11 Jun 2023 08:46:32 +0900
parents 1f62d04b49f2
children ec6fc84284f7
files src/FLutil.agda src/FundamentalHomorphism.agda src/fin.agda src/sym5a.agda src/sym5n.agda
diffstat 5 files changed, 21 insertions(+), 9 deletions(-) [+]
line wrap: on
line diff
--- a/src/FLutil.agda	Sun Jan 29 21:59:08 2023 +0900
+++ b/src/FLutil.agda	Sun Jun 11 08:46:32 2023 +0900
@@ -2,7 +2,7 @@
 module FLutil where
 
 open import Level hiding ( suc ; zero )
-open import Data.Fin hiding ( _<_  ; _≤_ ; _-_ ; _+_ ; _≟_)
+open import Data.Fin hiding (_<_  ; _>_ ; _≤_ ; _-_ ; _+_ ; _≟_)
 open import Data.Fin.Properties hiding ( <-trans ; ≤-refl ; ≤-trans ; ≤-irrelevant ; _≟_ ) renaming ( <-cmp to <-fcmp )
 open import Data.Fin.Permutation  -- hiding ([_,_])
 open import Data.Nat -- using (ℕ; suc; zero; s≤s ; z≤n )
@@ -19,7 +19,7 @@
 
 infixr  100 _::_
 
-data  FL : (n : ℕ )→ Set where
+data  FL : (n : ℕ ) → Set where
    f0 :  FL 0 
    _::_ :  { n : ℕ } → Fin (suc n ) → FL n → FL (suc n)
 
--- a/src/FundamentalHomorphism.agda	Sun Jan 29 21:59:08 2023 +0900
+++ b/src/FundamentalHomorphism.agda	Sun Jun 11 08:46:32 2023 +0900
@@ -191,7 +191,7 @@
            φ-cong = ?
 
     inv-φ : Group.Carrier (G / K ) → Group.Carrier G
-    inv-φ f =  n f  
+    inv-φ f =  n f    -- ⟦ n f ⟧ ( if we have gk03 )
 
     cong-i : {f g : Group.Carrier (G / K ) } → ⟦ n f ⟧ ≈ ⟦ n g ⟧ → inv-φ f ≈ inv-φ g
     cong-i {f} {g} nf=ng = ? 
--- a/src/fin.agda	Sun Jan 29 21:59:08 2023 +0900
+++ b/src/fin.agda	Sun Jun 11 08:46:32 2023 +0900
@@ -2,7 +2,7 @@
 
 module fin where
 
-open import Data.Fin hiding (_<_ ; _≤_ )
+open import Data.Fin hiding (_<_ ; _≤_ ; _>_ )
 open import Data.Fin.Properties hiding ( <-trans )
 open import Data.Nat
 open import logic
--- a/src/sym5a.agda	Sun Jan 29 21:59:08 2023 +0900
+++ b/src/sym5a.agda	Sun Jun 11 08:46:32 2023 +0900
@@ -1,3 +1,6 @@
+--
+-- checking does not terminate, sorry
+--
 open import Level hiding ( suc ; zero )
 open import Algebra
 module sym5a where
--- a/src/sym5n.agda	Sun Jan 29 21:59:08 2023 +0900
+++ b/src/sym5n.agda	Sun Jun 11 08:46:32 2023 +0900
@@ -1,3 +1,5 @@
+{-# OPTIONS --guardedness #-}
+
 open import Level hiding ( suc ; zero )
 open import Algebra
 module sym5n where
@@ -19,6 +21,13 @@
 open import Data.Fin
 open import Data.Fin.Permutation hiding (_∘ₚ_)
 
+open import Data.Nat.Base
+open import Data.Nat.Show using (show)
+open import Data.String using (String; _++_; lines)
+open import Data.Unit.Polymorphic as DP hiding (⊤)
+open import IO
+
+
 infixr  200 _∘ₚ_
 _∘ₚ_ = Data.Fin.Permutation._∘ₚ_
 
@@ -59,12 +68,12 @@
    FListtoStr [] = ""
    FListtoStr (cons a x x₁) = primStringAppend (FLtoStr a) (primStringAppend "\n" (FListtoStr x))
 
-open import Codata.Musical.Notation
+-- open import Codata.Musical.Notation
 open import Data.Maybe hiding (_>>=_)
 open import Data.List  
 open import Data.Char  
-open import IO.Primitive
-open import Codata.Musical.Costring
+-- open import IO.Primitive
+-- open import Codata.Musical.Costring
 
 postulate
     getArgs : IO (List (List Char))
@@ -97,7 +106,7 @@
 -- agda --compile sym5n.agda
 --
 
-main : IO ⊤
-main = getArgs >>= (λ x →  putStrLn $ toCostring $ sym5solvable $ getNumArg1 x ) 
+main : IO {0ℓ} DP.⊤
+main = getArgs >>= (λ x →  putStrLn $ sym5solvable $ getNumArg1 x )