@@ -27,7 +27,8 @@ public export
2727data Split : List a -> Type where
2828 SplitNil : Split []
2929 SplitOne : Split [x]
30− SplitPair : Split (x :: xs ++ y :: ys)
30+ SplitPair : {x, y : a} -> {xs, ys : List a} -> -- Explicit, don't erae
31+ Split (x :: xs ++ y :: ys)
3132
3233splitHelp : (head : a) ->
3334 (xs : List a) ->
@@ -53,8 +54,9 @@ split (x :: xs) = splitHelp x xs xs
5354public export
5455data SplitRec : List a -> Type where
5556 SplitRecNil : SplitRec []
56− SplitRecOne : SplitRec [x]
57− SplitRecPair : Lazy (SplitRec xs) -> Lazy (SplitRec ys) -> SplitRec (xs ++ ys)
57+ SplitRecOne : {x : a} -> SplitRec [x]
58+ SplitRecPair : {xs, ys : List a} -> -- Explicit, don't erase
59+ Lazy (SplitRec xs) -> Lazy (SplitRec ys) -> SplitRec (xs ++ ys)
5860
5961total
6062splitRecFix : (xs : List a) -> ((ys : List a) -> smaller ys xs -> SplitRec ys) ->
@@ -76,7 +78,8 @@ splitRec xs = accInd splitRecFix xs (smallerAcc xs)
7678public export
7779data SnocList : List a -> Type where
7880 Empty : SnocList []
79− Snoc : SnocList xs -> SnocList (xs ++ [x])
81+ Snoc : {x : a} -> {xs : List a} -> -- Explicit, so don't erase
82+ SnocList xs -> SnocList (xs ++ [x])
8083
8184snocListHelp : SnocList xs -> (ys : List a) -> SnocList (xs ++ ys)
8285snocListHelp {xs} x [] = rewrite appendNilRightNeutral xs in x