Report a paste

Please put a quick comment for the admin.

If it looks like spam, the admin will mark it as spam so that the spam filter picks it up in the future.

If the paste contains something private or offensive, it'll probably just be deleted.

Insert

import Data.Vect

data Insert : elem -> Vect n elem -> Vect (S n) elem -> Type where
  IHere : Insert x xs (x :: xs)
  ILater : Insert x xs ys -> Insert x (m :: xs) (m :: ys)

total
insert_append : (as : Vect n elem) -> (x : elem) -> (bs : Vect m elem) -> Insert x (as ++ bs) (rewrite plusSuccRightSucc n m in as ++ x :: bs)
insert_append [] x bs = IHere
insert_append {n = S k} {m} (a :: as) x bs =
  let IH = insert_append as x bs
  in ILater {m = a} {x = x} {xs = as ++ bs} {ys = rewrite plusSuccRightSucc k m in as ++ x :: bs} (?cvt)