Mercurial > hg > Members > kono > Proof > galois

changeset 136:5689c06be30d

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 Tue, 08 Sep 2020 13:51:10 +0900
parents 4e2d272b4bcc
children 1722fd0f1fcf
files FL.agda
diffstat 1 files changed, 4 insertions(+), 11 deletions(-) [+]
line wrap: on
line diff
--- a/FL.agda	Tue Sep 08 12:29:58 2020 +0900
+++ b/FL.agda	Tue Sep 08 13:51:10 2020 +0900
@@ -160,17 +160,10 @@
 FLcons {suc n} x [] = x ∷# []
 FLcons {suc n} x (cons a y x₁) with total x a
 ... | inj₁ (case1 eq) = cons a y x₁
-... | inj₁ (case2 lt) = cons x (cons a y x₁) ( Level.lift ttt , ttf ) where
-   tty :  fresh (FL (suc n)) ⌊ _f<?_ ⌋  a y
-   tty = x₁
-   ttf :  fresh (FL (suc n)) ⌊ _f<?_ ⌋  x y
-   ttf = {!!}
-   tt1 : true ≡ isYes (x f<? a)
-   tt1 with x f<? a
-   ... | yes y = refl
-   ... | no n = ⊥-elim ( n lt )
-   ttt :  T (isYes (x f<? a ))
-   ttt = subst (λ k → Data.Bool.T k ) tt1 tt
+FLcons {suc n} x (cons a y x₁) | inj₁ (case2 lt) = cons x ( cons a y x₁) ( {!!} , ttf a y  x₁) where
+   ttf : (a : FL (suc n)) → (y : FList {suc n}) →  fresh (FL (suc n)) ⌊ _f<?_ ⌋  a y  → fresh (FL (suc n)) ⌊ _f<?_ ⌋  x y
+   ttf a [] fr = Level.lift tt
+   ttf a (cons a₁ y x) fr = {!!}  , ttf a₁ y x
 ... | inj₂ (case1 eq) = cons a y x₁
 ... | inj₂ (case2 lt) = cons a (cons x y {!!}) {!!}