order = enum {greater, equal, lesser}
comparator<a> = (a,a)order

@assert pure, terminates
fn sorted<a>(pair (List<a>,comparator<a>))bool {
  (l, cmp) = pair
  if l.length() <= 1 {
    return true
  }
  return cmp(l[0],l[1]) != order.greater & sorted(l.tail())
}


SortedList<a> = (List<a>,(a,a)order) & sorted

@assert pure, terminates
fn empty(l SortedList<a>) bool {
  l[0].empty()
}

@assert pure, terminates
fn join<a>(start SortedList<a>,end SortedList<a>)SortedList<a>{
  assert: start[1] == end[1] // Comparators must be the same for this to make sense
  if start.empty() {
    return end
  }
  if end.empty(){
    return start
  }
  assert: start[1](start[0].last(),end[0].head()) != order.greater // can't make a sorted list by joining them
  return (start[0].join(end[0]), start[1])
}

@assert pure, terminates
fn insert<a>(list SortedList<a>, element a) SortedList<a>{
  // You get the idea
}

@assert pure, terminates
fn insertionSort<a>(l List<a>, cmp (a,a)order) SortedList<a> {
  if l.empty() {
    return ([],cmp)
  }
  out SortedList<a> = (l,cmp)
  for element in l {
     out = out.insert(element)
  }
  return out
}

fn commutative<a,b>(f (a,a)b){
  assert x,y: f(x,y) == f(y,x)
}

XY = (int, int)

@assert commutative
fn add(a XY, b XY) XY {
  return (a[0]+b[0], a[1] + b[1])
}

assert x: add(x,(0,0)) == x