module Data.Binary.Definition where

infixr 8 1แต‡_ 2แต‡_
data ๐”น : Set where
  0แต‡ : ๐”น
  1แต‡_ 2แต‡_ : ๐”น โ†’ ๐”น