view UInt {
  source Binary
  target UIntView
  into uint_view
  out uint_unview
  roundtrip uint_view_unview
}

fun div2(b:UInt)

fun fromNat(Nat) -> UInt

fun log(b:UInt)

fun max(x:UInt, y:UInt) {
  if x < y then
    y
  else
    x
}

fun min(x:UInt, y:UInt) {
  if x < y then
    x
  else
    y
}

fun operator *(UInt,UInt) -> UInt

fun operator +(UInt,UInt) -> UInt

fun operator <(UInt,UInt) -> bool

fun operator >(x:UInt, y:UInt) {
  y < x
}

fun operator ^(a:UInt, b:UInt)

fun operator ∸(UInt,UInt) -> UInt

fun operator ≤(x:UInt, y:UInt) {
  ((x < y) or (x = y))
}

fun operator ≥(x:UInt, y:UInt) {
  y ≤ x
}

fun sqr(a:UInt) {
  a * a
}

fun toNat(UInt) -> Nat