BV.agda

{-# OPTIONS --no-unicode #-}
module BV where

data Two : Set where
  ff tt : Two

data BV : Set where
  end : BV
  _-,_ : BV -> Two -> BV

infixl 10 _-,_

suc : BV -> BV
suc end = end -, tt
suc (xs -, ff) = xs -, tt
suc (xs -, tt) = suc xs -, ff

idOrSuc : Two -> Two -> BV -> BV
idOrSuc tt tt xs = suc xs
idOrSuc _ _ xs = xs

xor : Two -> Two -> Two
xor ff ff = ff
xor ff tt = tt
xor tt ff = tt
xor tt tt = ff

_+B_ : BV -> BV -> BV
end +B ys = ys
xs@(_ -, _) +B end = xs
(xs -, x) +B (ys -, y) = idOrSuc x y (xs +B ys) -, xor x y