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

opaque define div2 : (fn UInt -> UInt)

opaque recursive fromNat(Nat) -> UInt

opaque define log : (fn UInt -> UInt)

define max : (fn (UInt, UInt) -> UInt) = fun x:UInt, y:UInt {
      if x < y then
        y
      else
        x
    }

define min : (fn (UInt, UInt) -> UInt) = fun x:UInt, y:UInt {
      if x < y then
        x
      else
        y
    }

opaque recursive operator *(UInt,UInt) -> UInt

opaque recursive operator +(UInt,UInt) -> UInt

opaque recursive operator <(UInt,UInt) -> bool

define operator > : (fn (UInt, UInt) -> bool) = fun x:UInt, y:UInt {
      y < x
    }

opaque define operator ^ : (fn (UInt, UInt) -> UInt)

opaque recursive operator ∸(UInt,UInt) -> UInt

define operator ≤ : (fn (UInt, UInt) -> bool) = fun x:UInt, y:UInt {
      ((x < y) or (x = y))
    }

define operator ≥ : (fn (UInt, UInt) -> bool) = fun x:UInt, y:UInt {
      y ≤ x
    }

define sqr : (fn UInt -> UInt) = fun a:UInt {
      a * a
    }

opaque recursive toNat(UInt) -> Nat