module UInt
import Base
import Nat
public import UIntDefs
public import UIntToFrom
public import UIntLess
public import UIntAdd
public import UIntMult
public import UIntMonus
public import UIntDiv
public import UIntPowLog
public import UIntEvenOdd
// Need lit, zero, and suc for unsigned integer literals.
export lit
export zero
export suc
// Declaring at the end of the library, so that
inductive UInt by uint_induction