Mercurial > hg > Members > kono > Proof > galois
changeset 243:326221cf402b
...
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Thu, 10 Dec 2020 12:06:33 +0900 |
| parents | 1a08ad5d0b4e |
| children | f1f76eed9335 |
| files | FLComm.agda |
| diffstat | 1 files changed, 7 insertions(+), 5 deletions(-) [+] |
line wrap: on
line diff
--- a/FLComm.agda Thu Dec 10 09:53:52 2020 +0900 +++ b/FLComm.agda Thu Dec 10 12:06:33 2020 +0900 @@ -185,14 +185,16 @@ anyFL01 : (n : ℕ) → AnyFL (suc n) anyFL01 zero = record { allFL = (zero :: f0) ∷# [] ; anyP = {!!} } -anyFL01 (suc n) = record { allFL = commList anyFL02 ; anyP = {!!} } where +anyFL01 (suc n) = record { allFL = ? commList (anyFL02 (suc n)) ; anyP = {!!} } where anyFL04 : (n : ℕ) → AnyFin n anyFL04 0 = record { allFin = zero :: f0 ∷# [] ; anyF = {!!} } anyFL04 (suc n) = record { allFin = {!!} ; anyF = {!!} } - anyFL02 : {!!} - anyFL02 = anyComm (allFin (anyFL04 (suc n))) (allFL (anyFL01 n)) (λ p q → FLpos p :: q) - anyFL03 : {!!} - anyFL03 = commAny anyFL02 + anyFL02 : (n : ℕ ) → AnyComm (allFin (anyFL04 (suc n))) (allFL (anyFL01 n)) (λ p q → FLpos p :: q ) + anyFL02 n = anyComm (allFin (anyFL04 (suc n))) (allFL (anyFL01 n)) (λ p q → FLpos p :: q) + anyFL03 : (n : ℕ ) → (x : FL (suc (suc n))) → Any (_≡_ x) (commList (anyFL02 n)) + anyFL03 zero x = {!!} + anyFL03 n (x :: y) with commAny (anyFL02 (suc n)) ({!!} :: FL0) {!!} {!!} --(anyFL03 {!!}) + ... | t = {!!} CommFListN : ℕ → FList n CommFListN zero = allFL (anyFL n)