@@ -95,6 +95,10 @@ data SubList : List a -> List a -> Type where
95 SubNil : SubList [] xs
95 SubNil : SubList [] xs
96 InList : SubElem x ys -> SubList xs ys -> SubList (x :: xs) ys
96 InList : SubElem x ys -> SubList xs ys -> SubList (x :: xs) ys
98+Uninhabited (SubElem x []) where
99+ uninhabited Z impossible
100+ uninhabited (S _) impossible
98-- Some useful hints for proof construction in polymorphic programs
102-- Some useful hints for proof construction in polymorphic programs
100public export total
104public export total
@@ -150,9 +154,9 @@ envElem Z (x :: xs) = [x]
150envElem (S k) (x :: xs) = envElem k xs
154envElem (S k) (x :: xs) = envElem k xs
152||| make an environment corresponding to a sub-list
156||| make an environment corresponding to a sub-list
153−%assert_total dropEnv : Env m ys -> SubList xs ys -> Env m xs
157+total dropEnv : Env m ys -> SubList xs ys -> Env m xs
154dropEnv [] SubNil = []
158dropEnv [] SubNil = []
155−-- dropEnv [] (InList y z) impossible
159+dropEnv [] (InList idx rest) = absurd idx
156dropEnv (y::ys) SubNil = []
160dropEnv (y::ys) SubNil = []
157dropEnv e@(y::ys) (InList idx rest) =
161dropEnv e@(y::ys) (InList idx rest) =
158 let [x] = envElem idx e
162 let [x] = envElem idx e