    ------------------------------------------------------------------------
    -- The Agda standard library
    --
    -- Natural numbers represented in binary natively in Agda.
    ------------------------------------------------------------------------

    {-# OPTIONS --cubical-compatible --safe #-}

    module Data.Nat.Binary where

    open import Data.Nat.Binary.Base public
    open import Data.Nat.Binary.Properties public using (_≟_)