Hans-J. Schmid (14) [Avatar] Offline
#1
I do not understand the meaning of {x=y} in the merge sort example. Where does the 'y' actually come from?

total
splitList : (xs : List a) ->  SplitList xs
splitList xs = splitListHelp xs xs
  where
    splitListHelp : (counter : List a) -> (xs : List a) -> SplitList xs
    splitListHelp _ [] = SplitNil
    splitListHelp _ [x] = SplitOne
    splitListHelp (_ :: _ :: ys) (x :: xs)
       = case splitListHelp ys xs of
              SplitNil => SplitOne
              SplitOne {x=y} => SplitPair [x] [y]                                               -- What does {x=y} mean?
              SplitPair lefts rights => SplitPair (x :: lefts) rights
    splitListHelp _ xs = SplitPair [] xs
Edwin Brady (65) [Avatar] Offline
#2
It's a pattern match on the implicit argument with the name 'x', and the pattern being matched is 'y'. This is explained in more detail at the end of Chapter 3 in the section on implicit arguments (Section 3.4).
Hans-J. Schmid (14) [Avatar] Offline
#3
Ok. Got it. Stupid me. smilie

Thanks a lot, Edwin!