Mercurial > hg > Members > kono > Proof > galois

comparison FL.agda @ 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
comparison
equal deleted inserted replaced
135:4e2d272b4bcc 136:5689c06be30d
158 FLcons : {n : ℕ } → FL n → FList {n} → FList {n} 158 FLcons : {n : ℕ } → FL n → FList {n} → FList {n}
159 FLcons {zero} f0 y = f0 ∷# [] 159 FLcons {zero} f0 y = f0 ∷# []
160 FLcons {suc n} x [] = x ∷# [] 160 FLcons {suc n} x [] = x ∷# []
161 FLcons {suc n} x (cons a y x₁) with total x a 161 FLcons {suc n} x (cons a y x₁) with total x a
162 ... | inj₁ (case1 eq) = cons a y x₁ 162 ... | inj₁ (case1 eq) = cons a y x₁
163 ... | inj₁ (case2 lt) = cons x (cons a y x₁) ( Level.lift ttt , ttf ) where 163 FLcons {suc n} x (cons a y x₁) | inj₁ (case2 lt) = cons x ( cons a y x₁) ( {!!} , ttf a y x₁) where
164 tty : fresh (FL (suc n)) ⌊ _f<?_ ⌋ a y 164 ttf : (a : FL (suc n)) → (y : FList {suc n}) → fresh (FL (suc n)) ⌊ _f<?_ ⌋ a y → fresh (FL (suc n)) ⌊ _f<?_ ⌋ x y
165 tty = x₁ 165 ttf a [] fr = Level.lift tt
166 ttf : fresh (FL (suc n)) ⌊ _f<?_ ⌋ x y 166 ttf a (cons a₁ y x) fr = {!!} , ttf a₁ y x
167 ttf = {!!}
168 tt1 : true ≡ isYes (x f<? a)
169 tt1 with x f<? a
170 ... | yes y = refl
171 ... | no n = ⊥-elim ( n lt )
172 ttt : T (isYes (x f<? a ))
173 ttt = subst (λ k → Data.Bool.T k ) tt1 tt
174 ... | inj₂ (case1 eq) = cons a y x₁ 167 ... | inj₂ (case1 eq) = cons a y x₁
175 ... | inj₂ (case2 lt) = cons a (cons x y {!!}) {!!} 168 ... | inj₂ (case2 lt) = cons a (cons x y {!!}) {!!}
176 169
177 fr6 = FLcons ((# 1) :: ((# 1) :: ((# 0 ) :: f0))) fr1 170 fr6 = FLcons ((# 1) :: ((# 1) :: ((# 0 ) :: f0))) fr1