datatype list (a:t@ype, int) =
  | nil (a, 0)
  | {n:nat} cons (a, n+1) of (a, list (a, n))

fun{a:t@ype} list_length {n:nat} (xs: list (a, n)): int n = 
  case+ xs of
  | nil () => 0
  | cons (_, xs) => 1 + list_length(xs)

fun{a:t@ype} list_drop {m,n:nat | n <= m} (
  xs: list (a, m),
  count: int n
  ): list (a, m - n) =
  case+ xs of
  | nil () => nil ()
  | cons (x, xs2) => if count > 0 then list_drop(xs2, count - 1) else xs

implement main() = let
  val a = cons(1, cons(2, cons(3, cons(4, nil))))
  val b = list_drop(a, 2)
  val lena = list_length(a)
  val lenb = list_length(b)
  val () = printf("length a: %d\n", @(lena))
  val () = printf("length b: %d\n", @(lenb))
in
  ()
end