Mercurial > hg > Members > kono > Proof > galois

changeset 234:3c3619b196dc

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
allListF
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Wed, 09 Dec 2020 07:12:01 +0900
parents ff1e5a6e42da
children d204b7f9b89a
files FLComm.agda
diffstat 1 files changed, 4 insertions(+), 2 deletions(-) [+]
line wrap: on
line diff
--- a/FLComm.agda	Wed Dec 09 07:03:11 2020 +0900
+++ b/FLComm.agda	Wed Dec 09 07:12:01 2020 +0900
@@ -72,10 +72,12 @@
 anyFL (suc n)  = record { anyList = allListF a<sa []; anyP = {!!} } where 
     allListFL : (x : Fin (suc (suc n))) → FList (suc n) → FList (suc (suc n)) → FList (suc (suc n))
     allListFL _ [] y = y
-    allListFL x (cons y L yr) z = cons (x :: y) (allListFL x L z) {!!}
+    allListFL x (cons y L yr) z = FLinsert (x :: y) (allListFL x L z) 
     allListF : {i : ℕ} → (i<n : i < suc (suc n)) → FList (suc (suc n)) → FList (suc (suc n))
     allListF (s≤s z≤n) z = z
-    allListF (s≤s (s≤s i<n)) z = allListFL (fromℕ< {!!}) (anyList (anyFL n)) (allListF {!!} z)
+    allListF (s≤s (s≤s i<n)) z = allListFL (fin+1 (fromℕ< (s≤s i<n ))) (anyList (anyFL n)) (allListF (<-trans (s≤s i<n) a<sa) z)
+    anyFL0 :  (x : FL (suc (suc n))) → Any (_≡_ x) (allListF a<sa [])
+    anyFL0 = ?
 
 tl3 : (FL n) → ( z : FList n) → FList n → FList n
 tl3 h [] w = w