module UInt

import Base
import Nat

/*
  Public entry point for unsigned integers.

  This module re-exports the UInt representation-independent API:
  conversions to/from Nat, order, arithmetic, division, powers,
  logarithms, and parity facts. Import this module when proving about
  ordinary unsigned integer arithmetic.
*/

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
public import UIntSum

// Need lit, zero, and suc for unsigned integer literals.
export lit
export zero
export suc

// Declaring at the end of the library, so that the induction rule is
// available after the supporting UInt facts have been loaded.
inductive UInt by uint_induction