------------------------------------------------------------------------ -- 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)