Skip to content
Permalink
Branch: master
Find file Copy path
Find file Copy path
Fetching contributors…
Cannot retrieve contributors at this time
21 lines (16 sloc) 603 Bytes
{-# OPTIONS --without-K --safe #-}
module Data.Binary.Operations.Addition where
open import Data.Binary.Definitions
open import Data.Binary.Operations.Unary
add : Bit 𝔹⁺ 𝔹⁺ 𝔹⁺
add c (x ∷ xs) (y ∷ ys) = sumᵇ c x y ∷ add (carryᵇ c x y) xs ys
add O 1ᵇ ys = inc⁺⁺ ys
add O (O ∷ xs) 1= I ∷ xs
add O (I ∷ xs) 1= O ∷ inc⁺⁺ xs
add I 11= I ∷ 1
add I 1ᵇ (y ∷ ys) = y ∷ inc⁺⁺ ys
add I (x ∷ xs) 1= x ∷ inc⁺⁺ xs
_+_ : 𝔹 𝔹 𝔹
0ᵇ + ys = ys
(0< xs) + 0= 0< xs
(0< xs) + (0< ys) = 0< add O xs ys
You can’t perform that action at this time.