Mercurial > hg > Members > kono > Proof > galois

changeset 230:4cce0c52ec9f

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
...
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Tue, 08 Dec 2020 12:13:56 +0900
parents d3138997fe66
children 5a06df3e05d7
files FLComm.agda
diffstat 1 files changed, 7 insertions(+), 4 deletions(-) [+]
line wrap: on
line diff
--- a/FLComm.agda	Tue Dec 08 11:46:49 2020 +0900
+++ b/FLComm.agda	Tue Dec 08 12:13:56 2020 +0900
@@ -61,13 +61,16 @@
 open import fin
 open AnyFL
 anyFL :  AnyFL a<sa
-anyFL = record { anyList = FLinsert (fromℕ< a<sa :: fmax ) (anyListF fin<n) ; anyP = {!!} }  where
+anyFL  = record { anyList = FLinsert (fromℕ< a<sa :: fmax ) (anyListF {n} a<sa) ; anyP = {!!} }  where
   anyListFL : (P1 : FL n) → FList (suc n)
-  anyListFL (zero :: _)  = anyList anyFL 
-  anyListFL (suc p :: P1) =  FLinsert (fromℕ< a<sa  :: (suc p :: P1)) (anyListFL (fin+1 p :: P1))
+  anyListFL f0 = {!!}
+  anyListFL (zero :: y) = {!!}
+  anyListFL (suc x :: y) = {!!}
+  -- anyListFL (zero :: _)  = anyList anyFL 
+  -- anyListFL (suc p :: P1) =  FLinsert (fromℕ< a<sa  :: (suc p :: P1)) (anyListFL (fin+1 p :: P1))
   anyListF : {i : ℕ} → (Q1 : i < suc n) → FList (suc n)
   anyListF (s≤s z≤n) = anyListFL fmax
-  anyListF (s≤s (s≤s i<n)) = {!!} --FLinsert (fromℕ< (s≤s i<n) :: fmax) ? -- (anyListF (s≤s i<n) fmax)
+  anyListF (s≤s (s≤s i<n)) = FLinsert (fromℕ< {!!} :: fmax) (anyListF ? )
   
 
 tl3 : (FL n) → ( z : FList n) → FList n → FList n