module Data.Binary.Increment where

open import Data.Binary.Definition

inc : 𝔹  𝔹
inc 0ᵇ      = 1ᵇ 0ᵇ
inc (1ᵇ xs) = 2ᵇ xs
inc (2ᵇ xs) = 1ᵇ inc xs