datatype bool = false | true
typeref bool of nat
   with false <| bool(0) | true <| bool(1)

datatype 'a list = nil | cons of 'a * 'a list
typeref 'a list of nat
   with nil <| 'a list(0) | cons <| {n: nat} 'a * 'a list(n) -> 'a list(n+1)

datatype 'a option = NONE | SOME of 'a

datatype order = LESS | EQUAL | GREATER

assert abs <| {n: int} int(n) -> int(abs(n))
   and sgn <| {n: int} int(n) -> int(sgn(n))
   and succ <| {n:nat} int(n) -> int(n+1)
   and pred <| {n:nat | n > 0} int(n) -> int(n-1)
   and + <| {i:int, j:int} int(i) * int (j) -> int(i + j)
   and - <| {i:int, j:int} int(i) * int (j) -> int(i - j)
   and * <| {i:int, j:int} int(i) * int (j) -> int(i * j)
   and div <| {i:int, j:int} int(i) * int (j) -> int(i div j)
   and min <| {i:int, j:int} int(i) * int (j) -> int(min(i, j))
   and max <| {i:int, j:int} int(i) * int (j) -> int(max(i,j))
   and mod <| {i:int, j:int} int(i) * int (j) -> int(i mod j)

assert < <| {i:int, j:int} int(i) * int (j) -> bool(ls(i, j))
   and <= <| {i:int, j:int} int(i) * int (j) -> bool(lseq(i, j))
   and = <| {i:int, j:int} int(i) * int (j) -> bool(eq(i, j))
   and >= <| {i:int, j:int} int(i) * int (j) -> bool(lseq(j, i))
   and > <| {i:int, j:int} int(i) * int (j) -> bool(ls(j, i))
   and <> <| {i:int, j:int} int(i) * int (j) -> bool(neq(i, j))

assert print <| string -> unit
   and ^ <| string * string -> string

assert array <| {size:nat} int(size) * 'a -> 'a array(size)
   and subscript <| {size:nat, i:nat | i < size} 'a array(size) * int(i) -> 'a
   and update <| {size:nat, i:nat | i < size} 'a array(size) * int(i) * 'a -> unit
   and arraySize <| {n:nat} 'a array(n) -> int(n)

assert :: <| {n:nat} 'a * 'a list(n) -> 'a list(n+1)
   and @ <| {m:nat, n:nat} 'a list(m) * 'a list(n) -> 'a list(m+n)
   and rev <|  {n: nat} 'a list(n) -> 'a list(n)
   and listLength <| {n: nat} 'a list(n) -> int(n)
   and listTake <| {m:nat, n:nat | n <= m } 'a list(m) * int(n) -> 'a list(n)
   and listDrop <| {m:nat, n:nat | n <= m } 'a list(m) * int(n) -> 'a list(m-n)