Mercurial > hg > Members > kono > Proof > galois
changeset 231:5a06df3e05d7
allListFL
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Tue, 08 Dec 2020 12:26:47 +0900 |
| parents | 4cce0c52ec9f |
| children | 8f7c09ff96bd |
| files | FLComm.agda |
| diffstat | 1 files changed, 12 insertions(+), 11 deletions(-) [+] |
line wrap: on
line diff
--- a/FLComm.agda Tue Dec 08 12:13:56 2020 +0900 +++ b/FLComm.agda Tue Dec 08 12:26:47 2020 +0900 @@ -60,18 +60,19 @@ open import fin open AnyFL + +{-# TERMINATING #-} anyFL : AnyFL a<sa -anyFL = record { anyList = FLinsert (fromℕ< a<sa :: fmax ) (anyListF {n} a<sa) ; anyP = {!!} } where - anyListFL : (P1 : FL n) → FList (suc n) - 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ℕ< {!!} :: fmax) (anyListF ? ) - +anyFL = record { anyList = FLinsert (fromℕ< a<sa :: fmax ) (allListF {n} a<sa) ; anyP = anyFLP } where + allListFL : (P1 : FL n) → FList (suc n) + allListFL f0 = [] + allListFL (zero :: y) = cons (fromℕ< a<sa :: zero :: y) [] {!!} + allListFL (suc x :: y) = cons (fromℕ< a<sa :: suc x :: y) (allListFL (fin+1 x :: y)) {!!} + allListF : {i : ℕ} → (Q1 : i < suc n) → FList (suc n) + allListF (s≤s z≤n) = allListFL fmax + allListF (s≤s (s≤s i<n)) = cons (fin+1 (fromℕ< (s≤s i<n)) :: fmax) (allListF (<-trans (s≤s i<n) a<sa)) {!!} + anyFLP : (x : FL n) → Any (_≡_ (fromℕ< a<sa :: x)) (FLinsert (fromℕ< a<sa :: fmax) (allListF a<sa)) + anyFLP = {!!} tl3 : (FL n) → ( z : FList n) → FList n → FList n tl3 h [] w = w