Mercurial > hg > Members > kono > Proof > galois
changeset 158:8951ed37c1ab
...
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Fri, 18 Sep 2020 11:19:16 +0900 |
| parents | c47a7880f7b2 |
| children | 28a985c263dc |
| files | FLutil.agda |
| diffstat | 1 files changed, 6 insertions(+), 4 deletions(-) [+] |
line wrap: on
line diff
--- a/FLutil.agda Fri Sep 18 11:13:56 2020 +0900 +++ b/FLutil.agda Fri Sep 18 11:19:16 2020 +0900 @@ -240,12 +240,14 @@ af3 : (w : Fin (suc n)) (x y : FL n) → Level.Lift Level.zero (True (x f<? y )) → (w :: x ) f< (w :: y ) af3 w x y (Level.lift z) with x f<? y ... | yes x<y = f<t x<y - af4 : ( y : FList n ) → ( z : FList (suc n)) → FList (suc n) - af4 [] z = z - af4 (cons a y x) z = cons ( {!!} :: a ) (af4 y z) {!!} + af4 : ( y : FList n ) → ( z : FList (suc n)) → fresh (FL n) ⌊ _f<?_ ⌋ {!!} y → FList (suc n) + af4r : fresh (FL (suc n)) ⌊ _f<?_ ⌋ (? :: ?) (af4 ? ? ?) + af4 [] z _ = z + af4 (cons a y x) z _ = cons ( {!!} :: a ) (af4 y z {!!} ) {!!} + af4r = ? af1 : (i : ℕ ) → i ≤ suc n → FList (suc n) af1 zero i<n = Data.List.Fresh.map (zero ::_ ) (λ {x} {x₁} xr → Level.lift (fromWitness (af3 zero x x₁ xr ) )) (∀FListP.∀list af0 ) - af1 (suc i) (s≤s i<n) = af4 (∀FListP.∀list af0 ) ( af1 i (≤-trans i<n a≤sa)) + af1 (suc i) (s≤s i<n) = af4 (∀FListP.∀list af0 ) ( af1 i (≤-trans i<n a≤sa)) {!!} af2 : (x : FL (suc n)) → (y : FList (suc n)) → Any (_≡_ x) y af2 = {!!}