------------------------------------------------------------------------
-- The Agda standard library
--
-- Natural numbers
------------------------------------------------------------------------
 
-- See README.Data.Nat for examples of how to use and reason about
-- naturals.
 
{-# OPTIONS --cubical-compatible --safe #-}
 
module Data.Nat where
 
------------------------------------------------------------------------
-- Publicly re-export the contents of the base module
 
open import Data.Nat.Base public
 
------------------------------------------------------------------------
-- Publicly re-export queries
 
open import Data.Nat.Properties public
  using
  -- key values
  ( nonZero?
  -- equalities
  ; _≟_ ; eq?
  -- standard orders & their relationship
  ; _≤?_ ; _≥?_ ; _<?_ ; _>?_
  ; ≤-<-connex ; ≥->-connex ; <-≤-connex ; >-≥-connex
  ; <-cmp
  -- alternative definitions of the orders
  ; _≤′?_; _≥′?_; _<′?_; _>′?_
  ; _≤″?_; _<″?_; _≥″?_; _>″?_
  ; _<‴?_; _≤‴?_; _≥‴?_; _>‴?_
  -- bounded predicates
  ; anyUpTo? ; allUpTo?
  )
 
------------------------------------------------------------------------
-- Deprecated
 
-- Version 0.17
 
-- Version 2.0
 
-- solely for the re-export of this name, formerly in `Data.Nat.Properties.Core`
open import Data.Nat.Properties public
  using (≤-pred)