Mercurial > hg > Members > kono > Proof > galois

comparison FL.agda @ 139:065d8410d346

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 Wed, 09 Sep 2020 11:14:36 +0900
parents 6bb9b3f7b844
children 6006d2beaf24
comparison
equal deleted inserted replaced
138:6bb9b3f7b844 139:065d8410d346
170 ttf a _ [] fr = Level.lift tt 170 ttf a _ [] fr = Level.lift tt
171 ttf a lt (cons a₁ y x1) (lift lt1 , x2 ) = (Level.lift (fromWitness (ttf1 lt1 lt ))) , ttf a₁ (ttf1 lt1 lt) y x1 where 171 ttf a lt (cons a₁ y x1) (lift lt1 , x2 ) = (Level.lift (fromWitness (ttf1 lt1 lt ))) , ttf a₁ (ttf1 lt1 lt) y x1 where
172 ttf1 : True (a f<? a₁) → x f< a → x f< a₁ 172 ttf1 : True (a f<? a₁) → x f< a → x f< a₁
173 ttf1 t x<a = f<-trans x<a (toWitness t) 173 ttf1 t x<a = f<-trans x<a (toWitness t)
174 ... | inj₂ (case1 eq) = cons a y x₁ 174 ... | inj₂ (case1 eq) = cons a y x₁
175 ... | inj₂ (case2 lt) = cons a (cons x y (ttf2 a lt y x₁)) (Level.lift (fromWitness lt ) , x₁) where 175 ... | inj₂ (case2 lt) = cons a ( FLinsert x y ) (ttf2 y) where
176 ttf2 : (a : FL (suc n)) → a f< x → (y : FList {suc n}) → fresh (FL (suc n)) ⌊ _f<?_ ⌋ a y → fresh (FL (suc n)) ⌊ _f<?_ ⌋ x y 176 ttf2 : (y : FList {suc n}) → fresh (FL (suc n)) ⌊ _f<?_ ⌋ a (FLinsert x y)
177 ttf2 = {!!} 177 ttf2 [] with FLinsert x []
178 ... | [] = Level.lift tt
179 ... | cons a t x = {!!} , {!!}
180 ttf2 (cons a [] x) = {!!}
181 ttf2 (cons a (cons a₁ y x₁) x) = {!!}
178 182
179 fr6 = FLinsert ((# 1) :: ((# 1) :: ((# 0 ) :: f0))) fr1 183 fr6 = FLinsert ((# 1) :: ((# 1) :: ((# 0 ) :: f0))) fr1