The Author Online Book Forums are Moving

The Author Online Book Forums will soon redirect to Manning's liveBook and liveVideo. All book forum content will migrate to liveBook's discussion forum and all video forum content will migrate to liveVideo. Log in to liveBook or liveVideo with your Manning credentials to join the discussion!

Thank you for your engagement in the AoF over the years! We look forward to offering you a more enhanced forum experience.

Hans-J. Schmid (16) [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 (66) [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 (16) [Avatar] Offline
#3
Ok. Got it. Stupid me. smilie

Thanks a lot, Edwin!