Mercurial > hg > Members > kono > Proof > galois
changeset 142:435159e2897a
...
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Thu, 10 Sep 2020 20:55:19 +0900 |
| parents | 35c0b6878863 |
| children | 029a7885fe57 |
| files | FL.agda |
| diffstat | 1 files changed, 5 insertions(+), 4 deletions(-) [+] |
line wrap: on
line diff
--- a/FL.agda Thu Sep 10 20:25:31 2020 +0900 +++ b/FL.agda Thu Sep 10 20:55:19 2020 +0900 @@ -176,9 +176,10 @@ FLinsert {suc n} x (cons a [] x₁) | inj₂ (case2 lt) with FLinsert x [] | inspect ( FLinsert x ) [] ... | [] | () ... | cons a₁ t x₂ | e = cons a ( x ∷# [] ) ( Level.lift (fromWitness lt) , Level.lift tt ) -FLinsert {suc n} x (cons a (cons a₁ y x₂) (lift a<a₁ , fr-ay)) | inj₂ (case2 lt) = ttf2 a a₁ x (FLinsert x (cons a₁ y x₂)) where - ttf2 : {n : ℕ } → (a a₁ x : FL (suc n)) → ( y : FList {suc n} ) → FList {suc n} - ttf2 a a₁ x [] = cons a (cons x ( cons a₁ [] (Level.lift tt) ) {!!} ) {!!} - ttf2 a a₁ x (cons a₂ t x₁) = cons a ( cons a₂ t x₁) ( {!!} , ( ttf x a ? t {!!}) ) +FLinsert {suc n} x (cons a (cons a₁ y x₂) (lift a<a₁ , fr-ay)) | inj₂ (case2 lt) with FLinsert x (cons a₁ y x₂) +... | [] = cons a (cons x ( cons a₁ [] (Level.lift tt) ) {!!} ) {!!} +... | cons a₂ t x₁ = cons a ( cons a₂ t x₁) ( Level.lift (fromWitness (ttf2 {!!} {!!})) , ( ttf a₂ a (ttf2 {!!} {!!} ) t x₁ )) where + ttf2 : fresh (FL (suc n)) ⌊ _f<?_ ⌋ a y → fresh (FL (suc n)) ⌊ _f<?_ ⌋ a₂ t → a f< a₂ + ttf2 = {!!} fr6 = FLinsert ((# 1) :: ((# 1) :: ((# 0 ) :: f0))) fr1