# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1607397236 -32400
# Node ID 4cce0c52ec9f5df419abedc3e6c3837027911ac9
# Parent  d3138997fe665535576f0b62b1c8c1ce9f3f160f
...

diff -r d3138997fe66 -r 4cce0c52ec9f FLComm.agda
--- 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