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_filter {m:nat} (
  xs: list (a, m),
  f: a -<> bool
  ): [n:nat | n <= m] list (a, n) =
  case+ xs of
  | nil () => nil ()
  | cons (x, xs) => if f(x) then cons(x, list_filter(xs, f)) else list_filter(xs, f)

implement main() = let
  val a = cons(1, cons(2, cons(3, cons(4, nil))))
  val b = list_filter(a, lam x => x mod 2 = 0)
  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