vec.mbt

///|
type Zero

///|
type Succ[N]

///|
trait Nat {}

///|
pub impl Nat for Zero

///|
pub impl[N : Nat] Nat for Succ[N]

///|
type Vec[A, L] @list.T[A]

///|
pub fn[A] nil() -> Vec[A, Zero] {
  @list.empty()
}

///|
pub fn[A, L : Nat] cons(x : A, xs : Vec[A, L]) -> Vec[A, Succ[L]] {
  @list.construct(x, xs.inner())
}

///|
pub fn[A, L : Nat] tail(xs : Vec[A, Succ[L]]) -> Vec[A, L] {
  match xs.inner() {
    Empty => panic()
    More(_, tail~) => tail
  }
}

///|
pub fn[A, L : Nat] head(xs : Vec[A, Succ[L]]) -> A {
  match xs.inner() {
    Empty => panic()
    More(x, ..) => x
  }
}

vec_test.mbt

test {
  let xs = cons(1,cons(2,cons(3,nil())))
  let ys : Vec[Int,Zero]= nil()
  tail(xs) |> ignore
  tail(ys) 

}