How to compare two natural numbers in Agda with standard library (like N -> N -> Bool)?

Question

I can compare two natural numbers by writing comparator manually:

is-≤ : ℕ → ℕ → Bool
is-≤ zero _ = true
is-≤ (suc _) zero = false
is-≤ (suc x) (suc y) = is-≤ x y

However, I hope that there is something similar in the standard library so I don't write that every time.

I was able to find _≤_ operator in Data.Nat, but it's a parametrized type which basically contains "proof" that one specific number is less than the other (similar to _≡_). Is there a way to use it or something else to understand which number is smaller than the other "in runtime" (e.g. return corresponding Bool)?

The bigger problem I'm trying to solve:

1. As a part of my assignment, I'm writing a readNat : List Char → Maybe (ℕ × List Char) function. It tries to read natural number from the beginning of the list; will later become part of sscanf.
2. I want to implement digit : Char → Maybe ℕ helper function which would parse a single decimal digit.
3. In order to do so I want to compare primCharToNat c with primCharToNat '0', primCharToNat '1' and decide whether to return None or (primCharToNat c) ∸ (primCharToNat '0')

Answer 1

A solution suggested by @gallais in comments:

open import Data.Nat using (ℕ; _≤?_)
open import Data.Bool using (Bool)
open import Relation.Nullary using (Dec)

is-≤ : ℕ → ℕ → Bool
is-≤ a b with a ≤? b
... | Dec.yes _ = Bool.true
... | Dec.no _ = Bool.false

Here we match on a proof that _≤_ is decidable using the with-clause. One can use it similarly in more complex functions.

Suggestion by @user3237465 in comments to this answer: you can also use shorthand ⌊_⌋ (\clL/\clR or \lfloor/\rfloor) which does this exact pattern matching and eliminate the need for is-≤:

open import Data.Nat using (ℕ; _≤?_)
open import Data.Bool using (Bool)
open import Relation.Nullary.Decidable using (⌊_⌋)

is-≤ : ℕ → ℕ → Bool
is-≤ a b = ⌊ a ≤? b ⌋

Another approach is to use compare, it also provides more information (e.g. the difference between two numbers):

open import Data.Nat using (ℕ; compare)
open import Data.Bool using (Bool)
open import Relation.Nullary using (Dec)

is-≤' : ℕ → ℕ → Bool
is-≤' a b with compare a b
... | Data.Nat.greater _ _ = Bool.false
... | _ = Bool.true

is-≤3' : ℕ → Bool
is-≤3' a with 3 | compare a 3
... | _ | Data.Nat.greater _ _ = Bool.false
... | _ | _ = Bool.true

Note that compareing with a constant value requires extra caution for some reason.