list_append.out

fun {a:t@ype} list_append { m, n : nat }( xs : list(a, m)
                                        , ys : list(a, n)
                                        ) : list(a, m+n) =
  (case+ xs of
    | list_cons (x, xs) => list_cons((x, list_append(xs, ys)))
    | list_nil () => ys)

// end of [list_append]
fun {a:t@ype} list_append2 { m, n : nat }( xs : list(a, m)
                                         , ys : list(a, n)
                                         ) : list(a, m+n) =
  let
    //
    fun loop {m:nat}( xs : list(a, m)
                    , ys : list(a, n)
                    , res : &ptr? >> list(a, m+n)
                    ) : void =
      (case+ xs of
        | list_cons (x, xs1) => let
          val () = res := list_cons{a}{0}(x, _)
          val+ list_cons (_, res1) = res
          val () = loop((xs1, ys, res1))
          
          // of [xs1] and [ys]
        in
          fold@(res)
        end
        | list_nil () => res := ys)
    
    //
    var res: ptr
    val () = loop((xs, ys, res))
    
    //
  in
    res
  end

// end of [list_append2]