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

// Keep this explicit hook even though the public `induction UInt` case
// syntax is driven by the bijective view in UIntDefs. The view checker
// reuses uint_induction to supply the recursive successor IH, and the
// declaration also preserves the theorem-shaped custom induction fallback.
inductive UInt by uint_induction