termination.idr

-- Not fine:

  mergeBy : (a -> a -> Ordering) -> List a -> List a -> List a
  mergeBy order []      right   = right
  mergeBy order left    []      = left
  mergeBy order (x::xs) (y::ys) =
    case order x y of
      LT => x :: mergeBy order xs (y :: ys)
      _  => y :: mergeBy order (x :: xs) ys

-- Fine:

  mergeBy : (a -> a -> Ordering) -> List a -> List a -> List a
  mergeBy order []      right   = right
  mergeBy order left    []      = left
  mergeBy order (x::xs) (y::ys) =
    let rx = x::xs in
    let ry = y::ys in
    case order x y of
      LT => x :: mergeBy order xs ry
      _  => y :: mergeBy order rx ys