Mercurial > hg > Members > kono > Proof > galois

changeset 157:c47a7880f7b2

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
...
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Fri, 18 Sep 2020 11:13:56 +0900
parents 05fdfd07cabc
children 8951ed37c1ab
files FLutil.agda
diffstat 1 files changed, 4 insertions(+), 6 deletions(-) [+]
line wrap: on
line diff
--- a/FLutil.agda	Fri Sep 18 09:48:13 2020 +0900
+++ b/FLutil.agda	Fri Sep 18 11:13:56 2020 +0900
@@ -240,14 +240,12 @@
     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)  {!!} 
     af1 : (i : ℕ ) → i ≤ suc n  → FList (suc n)
-    af4 : (i : ℕ ) → (i<n : i ≤ n) → All {_} {_} {_} {_} {⌊ _f<?_ ⌋} (_# af1 i (≤-trans i<n a≤sa)) (Data.List.Fresh.map (fromℕ< (s≤s i<n) ::_)
-     (λ {x} {x₁} xr → Level.lift (fromWitness (af3 (fromℕ< (s≤s i<n)) x x₁ xr))) (∀FListP.∀list af0))
-    af4 = {!!}
     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) = append (Data.List.Fresh.map (fromℕ< (s≤s i<n) ::_ )
-             (λ {x} {x₁} xr → Level.lift (fromWitness (af3 (fromℕ< (s≤s i<n)) x x₁ xr ) )) (∀FListP.∀list af0 ))
-       (af1 i (≤-trans i<n a≤sa)) (af4 i i<n )
+    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 = {!!}